public class ProofTreeView extends javax.swing.JPanel implements KeYPaneExtension
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 |
javax.swing.JPanel.AccessibleJPanel
javax.swing.JComponent.AccessibleJComponent
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 |
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
ProofTreeView()
creates a new proof tree
|
ProofTreeView(KeYMediator m)
creates a new proof tree
|
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() |
getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI
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
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, 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
public static final java.awt.Color GRAY_COLOR
public static final java.awt.Color BISQUE_COLOR
public static final java.awt.Color LIGHT_BLUE_COLOR
public static final java.awt.Color DARK_BLUE_COLOR
public static final java.awt.Color DARK_GREEN_COLOR
public static final java.awt.Color DARK_RED_COLOR
public static final java.awt.Color PINK_COLOR
public static final java.awt.Color ORANGE_COLOR
public static final javax.swing.KeyStroke searchKeyStroke
public static final javax.swing.Icon PROOF_ICON
private static final long serialVersionUID
public final TacletInfoToggle tacletInfoToggle
final javax.swing.JTree delegateView
GUIProofTreeModel delegateModel
private KeYMediator mediator
private java.util.WeakHashMap<Proof,GUIProofTreeModel> models
private Proof proof
private ExpansionState expansionState
private ProofTreeView.GUIProofTreeProofListener proofListener
private ProofTreeView.GUITreeSelectionListener treeSelectionListener
private ProofTreeView.GUIProofTreeGUIListener guiListener
private ConfigChangeListener configChangeListener
private ImmutableList<Node> modifiedSubtrees
private java.util.HashSet<Node> modifiedSubtreesCache
private ProofTreeSearchBar proofTreeSearchPanel
public ProofTreeView(KeYMediator m)
public ProofTreeView()
protected void finalize() throws java.lang.Throwable
finalize
in class java.lang.Object
java.lang.Throwable
private void setProofTreeFont()
protected void layoutKeYComponent()
public KeYMediator getMediator()
private void setMediator(KeYMediator m)
private void register()
private void unregister()
public void removeNotify()
removeNotify
in class javax.swing.JComponent
private void setProof(Proof p)
p
- the Proof that has been loadedpublic void removeProofs(Proof[] ps)
public void makeNodeVisible(Node n)
protected void makeNodeExpanded(Node n)
protected void collapseClosedNodes()
private void collapseClosedNodesHelp(javax.swing.tree.TreePath path)
protected void collapseOthers(javax.swing.tree.TreePath path)
private void collapseOthersHelp(javax.swing.tree.TreePath start, javax.swing.tree.TreePath stop)
void selectBranchNode(GUIBranchNode node)
private void addModifiedNode(Node p_node)
public void showSearchPanel()
public void init(MainWindow window, KeYMediator mediator)
init
in interface KeYPaneExtension
public java.lang.String getTitle()
KeYPaneExtension
getTitle
in interface KeYPaneExtension
public javax.swing.Icon getIcon()
KeYPaneExtension
getIcon
in interface KeYPaneExtension
public javax.swing.JComponent getComponent()
KeYPaneExtension
getComponent
in interface KeYPaneExtension
public int priority()
priority
in interface KeYPaneExtension