public class CurrentGoalView extends SequentView implements Autoscroll
JEditorPane.AccessibleJEditorPane, JEditorPane.AccessibleJEditorPaneHTML, JEditorPane.JEditorPaneAccessibleHypertextSupport
JTextComponent.AccessibleJTextComponent, JTextComponent.DropLocation, JTextComponent.KeyBinding
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
static Color |
ADDITIONAL_HIGHLIGHT_COLOR |
private static Insets |
autoScrollSensitiveRegion |
static Color |
DEFAULT_HIGHLIGHT_COLOR |
static Color |
DND_HIGHLIGHT_COLOR |
private DragSource |
dragSource |
private int |
lastHighlightedCaretPos |
private CurrentGoalViewListener |
listener |
private KeYMediator |
mediator |
private static long |
serialVersionUID |
private static Color |
UPDATE_HIGHLIGHT_COLOR |
private LinkedList<Object> |
updateHighlights |
dndHighlight, filter, INACTIVE_BACKGROUND_COLOR, refreshHighlightning
HONOR_DISPLAY_PROPERTIES, W3C_LENGTH_UNITS
DEFAULT_KEYMAP, FOCUS_ACCELERATOR_KEY
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Constructor and Description |
---|
CurrentGoalView(MainWindow mainWindow)
creates a viewer for a sequent
|
Modifier and Type | Method and Description |
---|---|
void |
autoscroll(Point loc)
used for autoscrolling when performing drag and drop actions.
|
Insets |
getAutoscrollInsets()
used to define the area in which autoscrolling will be initialized
|
protected DragSource |
getDragSource() |
String |
getHighlightedText() |
KeYMediator |
getMediator()
returns the mediator of this view
|
PosInSequent |
getMousePosInSequent() |
protected SequentPrintFilter |
getSequentPrintFilter() |
String |
getTitle() |
void |
highlight(Point p) |
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, getFirstStatementRange, getHighlightedText, getHighlightRange, getLastPosInSequent, getLineWidth, getLogicPrinter, getMainWindow, getPosInSequent, getSyntaxHighlighter, getText, getVisibleTermLabels, paintHighlight, paintHighlights, removeHighlight, removeNotify, setCurrentHighlight, setFont, setLineWidth, setLogicPrinter, unregisterListener, 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 Color DEFAULT_HIGHLIGHT_COLOR
public static final Color ADDITIONAL_HIGHLIGHT_COLOR
private static final Color UPDATE_HIGHLIGHT_COLOR
public static final Color DND_HIGHLIGHT_COLOR
private final KeYMediator mediator
private final CurrentGoalViewListener listener
private DragSource dragSource
private static final Insets autoScrollSensitiveRegion
private final LinkedList<Object> updateHighlights
private int lastHighlightedCaretPos
public CurrentGoalView(MainWindow mainWindow)
mainWindow
- the MainWindow allowing access to the current system
statusvoid updateUpdateHighlights()
protected DragSource getDragSource()
public void printSequent()
printSequent
in class SequentView
void printSequentImmediately()
public void highlight(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 String getHighlightedText()
getHighlightedText
in class SequentView
public PosInSequent getMousePosInSequent()
public void autoscroll(Point loc)
autoscroll
in interface Autoscroll
public Insets getAutoscrollInsets()
getAutoscrollInsets
in interface Autoscroll
public String getTitle()
getTitle
in class SequentView