de.uka.ilkd.key.gui.nodeviews

Class CurrentGoalView

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.text.JTextComponent

javax.swing.JEditorPane

de.uka.ilkd.key.gui.nodeviews.SequentView

de.uka.ilkd.key.gui.nodeviews.CurrentGoalView

All Implemented Interfaces:

java.awt.dnd.Autoscroll, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible, javax.swing.Scrollable

public class CurrentGoalView
extends SequentView
implements java.awt.dnd.Autoscroll

This sequent view displays the sequent of an open goal and allows selection of formulas as well as the application of rules. It offers services for highlighting formulas, selecting applicable rules (in particular taclets) and drag'n drop instantiation of taclets.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.gui.nodeviews.SequentView

SequentView.PIO_age

Nested classes/interfaces inherited from class javax.swing.JEditorPane

javax.swing.JEditorPane.AccessibleJEditorPane, javax.swing.JEditorPane.AccessibleJEditorPaneHTML, javax.swing.JEditorPane.JEditorPaneAccessibleHypertextSupport

Nested classes/interfaces inherited from class javax.swing.text.JTextComponent

javax.swing.text.JTextComponent.AccessibleJTextComponent, javax.swing.text.JTextComponent.DropLocation, javax.swing.text.JTextComponent.KeyBinding

Nested classes/interfaces inherited from class javax.swing.JComponent

javax.swing.JComponent.AccessibleJComponent

Nested classes/interfaces inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.gui.nodeviews.SequentView

dndHighlight, filter, INACTIVE_BACKGROUND_COLOR, refreshHighlightning

Fields inherited from class javax.swing.JEditorPane

HONOR_DISPLAY_PROPERTIES, W3C_LENGTH_UNITS

Fields inherited from class javax.swing.text.JTextComponent

DEFAULT_KEYMAP, FOCUS_ACCELERATOR_KEY

Fields inherited from class javax.swing.JComponent

listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

Fields inherited from class java.awt.Component

accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

Constructors

Constructor and Description
CurrentGoalView(MainWindow mainWindow) creates a viewer for a sequent

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.gui.nodeviews.SequentView

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

Methods inherited from class javax.swing.JEditorPane

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

Methods inherited from class javax.swing.text.JTextComponent

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

Methods inherited from class javax.swing.JComponent

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

Methods inherited from class java.awt.Container

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

Methods inherited from class java.awt.Component

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

Methods inherited from class java.lang.Object

clone, equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

DEFAULT_HIGHLIGHT_COLOR

public static final java.awt.Color DEFAULT_HIGHLIGHT_COLOR

ADDITIONAL_HIGHLIGHT_COLOR

public static final java.awt.Color ADDITIONAL_HIGHLIGHT_COLOR

UPDATE_HIGHLIGHT_COLOR

private static final java.awt.Color UPDATE_HIGHLIGHT_COLOR

DND_HIGHLIGHT_COLOR

public static final java.awt.Color DND_HIGHLIGHT_COLOR

mediator

private final KeYMediator mediator

listener

private final CurrentGoalViewListener listener

dragSource

private java.awt.dnd.DragSource dragSource

autoScrollSensitiveRegion

private static final java.awt.Insets autoScrollSensitiveRegion

updateHighlights

private final java.util.LinkedList<java.lang.Object> updateHighlights

lastHighlightedCaretPos

private int lastHighlightedCaretPos

Constructor Detail

CurrentGoalView

public CurrentGoalView(MainWindow mainWindow)

creates a viewer for a sequent

Parameters:

mainWindow - the MainWindow allowing access to the current system status

Method Detail

updateUpdateHighlights

void updateUpdateHighlights()

updates all updateHighlights. Firstly removes all displayed ones and then gets a new list of updates to highlight

jumpToIntroduction

public 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.

getDragSource

protected java.awt.dnd.DragSource getDragSource()

printSequent

public void printSequent()

sets the text being printed

Specified by:

printSequent in class SequentView

printSequentImmediately

void printSequentImmediately()

sets the text being printed

highlight

public void highlight(java.awt.Point p)

Overrides:

highlight in class SequentView

restorePosition

void restorePosition()

setPrinter

public void setPrinter(Goal goal)

sets the LogicPrinter to use

getSequentPrintFilter

protected SequentPrintFilter getSequentPrintFilter()

getMediator

public final KeYMediator getMediator()

returns the mediator of this view

Returns:

the KeYMediator

selectedTaclet

void selectedTaclet(TacletApp taclet,
                    PosInSequent pos)

selected rule to apply

Parameters:

taclet - the selected Taclet

pos - the PosInSequent describes the position where to apply the rule

setModalDragNDropEnabled

public void setModalDragNDropEnabled(boolean allowDragNDrop)

Enables drag'n'drop of highlighted subterms in the sequent window.

Parameters:

allowDragNDrop - enables drag'n'drop iff set to true.

modalDragNDropEnabled

public boolean modalDragNDropEnabled()

Checks whether drag'n'drop of highlighted subterms in the sequent window currently is enabled..

Returns:

true iff drag'n'drop is enabled.

getHighlightedText

public java.lang.String getHighlightedText()

Overrides:

getHighlightedText in class SequentView

getMousePosInSequent

public PosInSequent getMousePosInSequent()

autoscroll

public void autoscroll(java.awt.Point loc)

used for autoscrolling when performing drag and drop actions. Computes the rectangle to be made visible.

Specified by:

autoscroll in interface java.awt.dnd.Autoscroll

getAutoscrollInsets

public java.awt.Insets getAutoscrollInsets()

used to define the area in which autoscrolling will be initialized

Specified by:

getAutoscrollInsets in interface java.awt.dnd.Autoscroll

getTitle

public java.lang.String getTitle()

Specified by:

getTitle in class SequentView