public class CurrentGoalView extends SequentView implements java.awt.dnd.Autoscroll
SequentView.PIO_age
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 java.awt.Color |
ADDITIONAL_HIGHLIGHT_COLOR |
private static java.awt.Insets |
autoScrollSensitiveRegion |
static java.awt.Color |
DEFAULT_HIGHLIGHT_COLOR |
static java.awt.Color |
DND_HIGHLIGHT_COLOR |
private java.awt.dnd.DragSource |
dragSource |
private int |
lastHighlightedCaretPos |
private CurrentGoalViewListener |
listener |
private KeYMediator |
mediator |
private static long |
serialVersionUID |
private static java.awt.Color |
UPDATE_HIGHLIGHT_COLOR |
private java.util.LinkedList<java.lang.Object> |
updateHighlights |
dndHighlight, filter, INACTIVE_BACKGROUND_COLOR, 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
|
(package private) void |
printSequentImmediately()
sets the text being printed
|
(package private) void |
restorePosition() |
(package private) void |
selectedTaclet(TacletApp taclet,
PosInSequent pos)
selected rule to apply
|
void |
setModalDragNDropEnabled(boolean allowDragNDrop)
Enables drag'n'drop of highlighted subterms in the sequent window.
|
void |
setPrinter(Goal goal)
sets the LogicPrinter to use
|
(package private) void |
updateUpdateHighlights()
updates all updateHighlights.
|
addNotify, computeLineWidth, correctedViewToModel, disableHighlight, disableHighlights, finalize, getColorHighlight, getCurrentHighlight, getFilter, getFirstStatementRange, getHighlightedText, getHighlightRange, getLastPosInSequent, getLineWidth, getLogicPrinter, getMainWindow, getPosInSequent, getSyntaxHighlighter, getText, getVisibleTermLabels, isHiding, paintHighlight, paintHighlights, removeHighlight, removeNotify, setCurrentHighlight, setFilter, setFont, setLineWidth, setLogicPrinter, 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, getToolTipText, 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
private static final long serialVersionUID
public static final java.awt.Color DEFAULT_HIGHLIGHT_COLOR
public static final java.awt.Color ADDITIONAL_HIGHLIGHT_COLOR
private static final java.awt.Color UPDATE_HIGHLIGHT_COLOR
public static final java.awt.Color DND_HIGHLIGHT_COLOR
private final KeYMediator mediator
private final CurrentGoalViewListener listener
private java.awt.dnd.DragSource dragSource
private static final java.awt.Insets autoScrollSensitiveRegion
private final java.util.LinkedList<java.lang.Object> updateHighlights
private int lastHighlightedCaretPos
public CurrentGoalView(MainWindow mainWindow)
mainWindow
- the MainWindow allowing access to the current system
statusvoid updateUpdateHighlights()
public Node jumpToIntroduction(Node node, SequentFormula form)
protected java.awt.dnd.DragSource getDragSource()
public void printSequent()
printSequent
in class SequentView
void printSequentImmediately()
public void highlight(java.awt.Point p)
highlight
in class SequentView
void restorePosition()
public void setPrinter(Goal goal)
protected SequentPrintFilter getSequentPrintFilter()
public final KeYMediator getMediator()
void selectedTaclet(TacletApp taclet, PosInSequent pos)
taclet
- the selected Tacletpos
- the PosInSequent describes the position where to apply the
rulepublic 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