public final class CurrentGoalView extends SequentView implements java.awt.dnd.Autoscroll
javax.swing.JEditorPane.AccessibleJEditorPane, javax.swing.JEditorPane.AccessibleJEditorPaneHTML, javax.swing.JEditorPane.JEditorPaneAccessibleHypertextSupport
javax.swing.text.JTextComponent.AccessibleJTextComponent, javax.swing.text.JTextComponent.DropLocation, javax.swing.text.JTextComponent.KeyBinding
javax.swing.JComponent.AccessibleJComponent
Modifier and Type | Field and Description |
---|---|
static ColorSettings.ColorProperty |
ADDITIONAL_HIGHLIGHT_COLOR |
static ColorSettings.ColorProperty |
DEFAULT_HIGHLIGHT_COLOR |
static ColorSettings.ColorProperty |
DND_HIGHLIGHT_COLOR |
dndHighlight, filter, INACTIVE_BACKGROUND_COLOR, OUTSIDE_MOUSE_POSITION, PERMANENT_HIGHLIGHT_COLOR, PROP_LAST_MOUSE_POSITION, refreshHighlightning
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
CurrentGoalView(MainWindow mainWindow)
creates a viewer for a sequent
|
Modifier and Type | Method and Description |
---|---|
void |
autoscroll(java.awt.Point loc)
used for autoscrolling when performing drag and drop actions.
|
java.awt.Insets |
getAutoscrollInsets()
used to define the area in which autoscrolling will be initialized
|
protected java.awt.dnd.DragSource |
getDragSource() |
java.lang.String |
getHighlightedText() |
KeYMediator |
getMediator()
returns the mediator of this view
|
PosInSequent |
getMousePosInSequent() |
protected SequentPrintFilter |
getSequentPrintFilter() |
java.lang.String |
getTitle() |
void |
highlight(java.awt.Point p) |
Node |
jumpToIntroduction(Node node,
SequentFormula form)
given a node and a sequent formula, returns the first node
among the node's parents that contains the sequent formula @form.
|
boolean |
modalDragNDropEnabled()
Checks whether drag'n'drop of highlighted subterms in the sequent window
currently is enabled..
|
void |
printSequent()
sets the text being printed
|
void |
setModalDragNDropEnabled(boolean allowDragNDrop)
Enables drag'n'drop of highlighted subterms in the sequent window.
|
void |
setPrinter(Goal goal)
sets the LogicPrinter to use
|
addNotify, computeLineWidth, correctedViewToModel, disableHighlight, disableHighlights, finalize, getColorHighlight, getCurrentHighlight, getFilter, getFirstStatementRange, getHighlightedText, getLastPosInSequent, getLineWidth, getLogicPrinter, getMainWindow, getPosInSequent, getSyntaxHighlighter, getText, getToolTipText, getVisibleTermLabels, isHiding, isInUserSelectionHighlight, isMainSequentView, paintHighlight, paintHighlights, removeHighlight, removeNotify, removeUserSelectionHighlight, setCurrentHighlight, setFilter, setFont, setLineWidth, setLogicPrinter, setUserSelectionHighlight, setUserSelectionHighlight, unregisterListener, updateHeatMapHighlights, updateHeatmapSFHighlights, updateHeatmapTermHighlights, updateHidingProperty, updateUI
addHyperlinkListener, createDefaultEditorKit, createEditorKitForContentType, fireHyperlinkUpdate, getAccessibleContext, getContentType, getEditorKit, getEditorKitClassNameForContentType, getEditorKitForContentType, getHyperlinkListeners, getPage, getPreferredSize, getScrollableTracksViewportHeight, getScrollableTracksViewportWidth, getStream, getUIClassID, paramString, read, registerEditorKitForContentType, registerEditorKitForContentType, removeHyperlinkListener, replaceSelection, scrollToReference, setContentType, setEditorKit, setEditorKitForContentType, setPage, setPage, setText
addCaretListener, addInputMethodListener, addKeymap, copy, cut, fireCaretUpdate, getActions, getCaret, getCaretColor, getCaretListeners, getCaretPosition, getDisabledTextColor, getDocument, getDragEnabled, getDropLocation, getDropMode, getFocusAccelerator, getHighlighter, getInputMethodRequests, getKeymap, getKeymap, getMargin, getNavigationFilter, getPreferredScrollableViewportSize, getPrintable, getScrollableBlockIncrement, getScrollableUnitIncrement, getSelectedText, getSelectedTextColor, getSelectionColor, getSelectionEnd, getSelectionStart, getText, getUI, isEditable, loadKeymap, modelToView, moveCaretPosition, paste, print, print, print, processInputMethodEvent, read, removeCaretListener, removeKeymap, restoreComposedText, saveComposedText, select, selectAll, setCaret, setCaretColor, setCaretPosition, setComponentOrientation, setDisabledTextColor, setDocument, setDragEnabled, setDropMode, setEditable, setFocusAccelerator, setHighlighter, setKeymap, setMargin, setNavigationFilter, setSelectedTextColor, setSelectionColor, setSelectionEnd, setSelectionStart, setUI, viewToModel, write
addAncestorListener, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update
add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusDownCycle, validate, validateTree
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
public static final ColorSettings.ColorProperty DEFAULT_HIGHLIGHT_COLOR
public static final ColorSettings.ColorProperty ADDITIONAL_HIGHLIGHT_COLOR
public static final ColorSettings.ColorProperty DND_HIGHLIGHT_COLOR
public CurrentGoalView(MainWindow mainWindow)
mainWindow
- the MainWindow allowing access to the current system
statuspublic Node jumpToIntroduction(Node node, SequentFormula form)
protected java.awt.dnd.DragSource getDragSource()
public void printSequent()
printSequent
in class SequentView
public void highlight(java.awt.Point p)
highlight
in class SequentView
public void setPrinter(Goal goal)
protected SequentPrintFilter getSequentPrintFilter()
public final KeYMediator getMediator()
public void setModalDragNDropEnabled(boolean allowDragNDrop)
allowDragNDrop
- enables drag'n'drop iff set to true.public boolean modalDragNDropEnabled()
public java.lang.String getHighlightedText()
getHighlightedText
in class SequentView
public PosInSequent getMousePosInSequent()
public void autoscroll(java.awt.Point loc)
autoscroll
in interface java.awt.dnd.Autoscroll
public java.awt.Insets getAutoscrollInsets()
getAutoscrollInsets
in interface java.awt.dnd.Autoscroll
public java.lang.String getTitle()
getTitle
in class SequentView
Copyright © 2003-2019 The KeY-Project.