de.uka.ilkd.key.gui.prooftree

Class ProofTreeView

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JPanel

de.uka.ilkd.key.gui.prooftree.ProofTreeView

All Implemented Interfaces:

KeYPaneExtension, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible

public class ProofTreeView
extends javax.swing.JPanel
implements KeYPaneExtension

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	ProofTreeView.CacheLessMetalTreeUI
(package private) class	ProofTreeView.GUIProofTreeGUIListener
(package private) class	ProofTreeView.GUIProofTreeProofListener
(package private) class	ProofTreeView.GUITreeSelectionListener
(package private) class	ProofTreeView.ProofRenderer
(package private) class	ProofTreeView.ProofTreePopupMenu

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

javax.swing.JPanel.AccessibleJPanel

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	BISQUE_COLOR
private ConfigChangeListener	configChangeListener
static java.awt.Color	DARK_BLUE_COLOR
static java.awt.Color	DARK_GREEN_COLOR
static java.awt.Color	DARK_RED_COLOR
(package private) GUIProofTreeModel	delegateModel the model that is displayed by the delegateView
(package private) javax.swing.JTree	delegateView The JTree that is used for actual display and interaction
private ExpansionState	expansionState the expansion state of the proof tree
static java.awt.Color	GRAY_COLOR
private ProofTreeView.GUIProofTreeGUIListener	guiListener
static java.awt.Color	LIGHT_BLUE_COLOR
private KeYMediator	mediator the mediator is stored here
private java.util.WeakHashMap<Proof,GUIProofTreeModel>	models
private ImmutableList<Node>	modifiedSubtrees Roots of subtrees containing all nodes to which rules have been applied; this is used when auto mode is active
private java.util.HashSet<Node>	modifiedSubtreesCache
static java.awt.Color	ORANGE_COLOR
static java.awt.Color	PINK_COLOR
private Proof	proof the proof this view shows
static javax.swing.Icon	PROOF_ICON
private ProofTreeView.GUIProofTreeProofListener	proofListener listener
private ProofTreeSearchBar	proofTreeSearchPanel the search dialog
static javax.swing.KeyStroke	searchKeyStroke KeYStroke for the search panel: STRG+SHIFT+F
private static long	serialVersionUID
TacletInfoToggle	tacletInfoToggle
private ProofTreeView.GUITreeSelectionListener	treeSelectionListener

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
ProofTreeView() creates a new proof tree
ProofTreeView(KeYMediator m) creates a new proof tree

Method Summary

Modifier and Type	Method and Description
private void	addModifiedNode(Node p_node) In auto mode, add a node which has been modified in a way leading to structural changes of the proof tree
protected void	collapseClosedNodes() Collapse all subtrees that are closed
private void	collapseClosedNodesHelp(javax.swing.tree.TreePath path)
protected void	collapseOthers(javax.swing.tree.TreePath path) Collapse all branches which are not below path
private void	collapseOthersHelp(javax.swing.tree.TreePath start, javax.swing.tree.TreePath stop)
protected void	finalize()
javax.swing.JComponent	getComponent() The content of the tab pane
javax.swing.Icon	getIcon() A nice icon for viewing aside to the tab title.
KeYMediator	getMediator() returns the mediator to communicate with the model
java.lang.String	getTitle() The title of the tab pane for the user.
void	init(MainWindow window, KeYMediator mediator)
protected void	layoutKeYComponent() layout the component
protected void	makeNodeExpanded(Node n)
void	makeNodeVisible(Node n) moves the scope of the tree view to the given node so that it is visible
int	priority()
private void	register()
void	removeNotify()
void	removeProofs(Proof[] ps)
(package private) void	selectBranchNode(GUIBranchNode node) Selects the given Branchnode in the ProofTreeView and displays the first child in the main view.
private void	setMediator(KeYMediator m) sets the mediator to communicate with the model
private void	setProof(Proof p) sets up the proof tree view if a proof has been loaded
private void	setProofTreeFont()
void	showSearchPanel()
private void	unregister()

Methods inherited from class javax.swing.JPanel

getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI

Methods inherited from class javax.swing.JComponent

addAncestorListener, addNotify, 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, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, 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, addInputMethodListener, 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, getInputMethodRequests, 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, processInputMethodEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, 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

GRAY_COLOR

public static final java.awt.Color GRAY_COLOR

BISQUE_COLOR

public static final java.awt.Color BISQUE_COLOR

LIGHT_BLUE_COLOR

public static final java.awt.Color LIGHT_BLUE_COLOR

DARK_BLUE_COLOR

public static final java.awt.Color DARK_BLUE_COLOR

DARK_GREEN_COLOR

public static final java.awt.Color DARK_GREEN_COLOR

DARK_RED_COLOR

public static final java.awt.Color DARK_RED_COLOR

PINK_COLOR

public static final java.awt.Color PINK_COLOR

ORANGE_COLOR

public static final java.awt.Color ORANGE_COLOR

searchKeyStroke

public static final javax.swing.KeyStroke searchKeyStroke

KeYStroke for the search panel: STRG+SHIFT+F

PROOF_ICON

public static final javax.swing.Icon PROOF_ICON

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

tacletInfoToggle

public final TacletInfoToggle tacletInfoToggle

delegateView

final javax.swing.JTree delegateView

The JTree that is used for actual display and interaction

delegateModel

GUIProofTreeModel delegateModel

the model that is displayed by the delegateView

mediator

private KeYMediator mediator

the mediator is stored here

models

private java.util.WeakHashMap<Proof,GUIProofTreeModel> models

proof

private Proof proof

the proof this view shows

expansionState

private ExpansionState expansionState

the expansion state of the proof tree

proofListener

private ProofTreeView.GUIProofTreeProofListener proofListener

listener

treeSelectionListener

private ProofTreeView.GUITreeSelectionListener treeSelectionListener

guiListener

private ProofTreeView.GUIProofTreeGUIListener guiListener

configChangeListener

private ConfigChangeListener configChangeListener

modifiedSubtrees

private ImmutableList<Node> modifiedSubtrees

Roots of subtrees containing all nodes to which rules have been applied; this is used when auto mode is active

modifiedSubtreesCache

private java.util.HashSet<Node> modifiedSubtreesCache

proofTreeSearchPanel

private ProofTreeSearchBar proofTreeSearchPanel

the search dialog

Constructor Detail

ProofTreeView

public ProofTreeView(KeYMediator m)

creates a new proof tree

ProofTreeView

public ProofTreeView()

creates a new proof tree

Method Detail

finalize

protected void finalize()
                 throws java.lang.Throwable

Overrides:

finalize in class java.lang.Object

Throws:

java.lang.Throwable

setProofTreeFont

private void setProofTreeFont()

layoutKeYComponent

protected void layoutKeYComponent()

layout the component

getMediator

public KeYMediator getMediator()

returns the mediator to communicate with the model

Returns:

the mediator to communicate with the model

setMediator

private void setMediator(KeYMediator m)

sets the mediator to communicate with the model

register

private void register()

unregister

private void unregister()

removeNotify

public void removeNotify()

Overrides:

removeNotify in class javax.swing.JComponent

setProof

private void setProof(Proof p)

sets up the proof tree view if a proof has been loaded

Parameters:

p - the Proof that has been loaded

removeProofs

public void removeProofs(Proof[] ps)

makeNodeVisible

public void makeNodeVisible(Node n)

moves the scope of the tree view to the given node so that it is visible

makeNodeExpanded

protected void makeNodeExpanded(Node n)

collapseClosedNodes

protected void collapseClosedNodes()

Collapse all subtrees that are closed

collapseClosedNodesHelp

private void collapseClosedNodesHelp(javax.swing.tree.TreePath path)

collapseOthers

protected void collapseOthers(javax.swing.tree.TreePath path)

Collapse all branches which are not below path

collapseOthersHelp

private void collapseOthersHelp(javax.swing.tree.TreePath start,
                                javax.swing.tree.TreePath stop)

selectBranchNode

void selectBranchNode(GUIBranchNode node)

Selects the given Branchnode in the ProofTreeView and displays the first child in the main view.

addModifiedNode

private void addModifiedNode(Node p_node)

In auto mode, add a node which has been modified in a way leading to structural changes of the proof tree

showSearchPanel

public void showSearchPanel()

init

public void init(MainWindow window,
                 KeYMediator mediator)

Specified by:

init in interface KeYPaneExtension

getTitle

public java.lang.String getTitle()

Description copied from interface: KeYPaneExtension

The title of the tab pane for the user.

Specified by:

getTitle in interface KeYPaneExtension

Returns:

non-null and non-empty string

getIcon

public javax.swing.Icon getIcon()

Description copied from interface: KeYPaneExtension

A nice icon for viewing aside to the tab title.

Specified by:

getIcon in interface KeYPaneExtension

Returns:

getComponent

public javax.swing.JComponent getComponent()

Description copied from interface: KeYPaneExtension

The content of the tab pane

Specified by:

getComponent in interface KeYPaneExtension

Returns:

priority

public int priority()

Specified by:

priority in interface KeYPaneExtension

Returns: