public class ProofTreeView extends JPanel
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 |
JPanel.AccessibleJPanel
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
static Color |
BISQUE_COLOR |
private ConfigChangeListener |
configChangeListener |
static Color |
DARK_BLUE_COLOR |
static Color |
DARK_GREEN_COLOR |
static Color |
DARK_RED_COLOR |
(package private) GUIProofTreeModel |
delegateModel
the model that is displayed by the delegateView
|
(package private) JTree |
delegateView
The JTree that is used for actual display and interaction
|
private ExpansionState |
expansionState
the expansion state of the proof tree
|
static Color |
GRAY_COLOR |
private ProofTreeView.GUIProofTreeGUIListener |
guiListener |
static Color |
LIGHT_BLUE_COLOR |
private KeYMediator |
mediator
the mediator is stored here
|
private 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 HashSet<Node> |
modifiedSubtreesCache |
static Color |
ORANGE_COLOR |
static Color |
PINK_COLOR |
private Proof |
proof
the proof this view shows
|
private ProofTreeView.GUIProofTreeProofListener |
proofListener
listener
|
private ProofTreeSearchBar |
proofTreeSearchPanel
the search dialog
|
static KeyStroke |
searchKeyStroke
KeYStroke for the search panel: STRG+SHIFT+F
|
private static long |
serialVersionUID |
TacletInfoToggle |
tacletInfoToggle |
private ProofTreeView.GUITreeSelectionListener |
treeSelectionListener |
accessibleContext, listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Constructor and Description |
---|
ProofTreeView(KeYMediator mediator)
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(TreePath path) |
protected void |
collapseOthers(TreePath path)
Collapse all branches which are not below path
|
private void |
collapseOthersHelp(TreePath start,
TreePath stop) |
protected void |
finalize() |
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
|
KeYMediator |
mediator()
returns the mediator to communicate with the model
|
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
private static final long serialVersionUID
public static final Color GRAY_COLOR
public static final Color BISQUE_COLOR
public static final Color LIGHT_BLUE_COLOR
public static final Color DARK_BLUE_COLOR
public static final Color DARK_GREEN_COLOR
public static final Color DARK_RED_COLOR
public static final Color PINK_COLOR
public static final Color ORANGE_COLOR
private KeYMediator mediator
final JTree delegateView
GUIProofTreeModel delegateModel
private WeakHashMap<Proof,GUIProofTreeModel> models
private Proof proof
private ExpansionState expansionState
private ProofTreeView.GUIProofTreeProofListener proofListener
private ProofTreeView.GUITreeSelectionListener treeSelectionListener
private ProofTreeView.GUIProofTreeGUIListener guiListener
public static final KeyStroke searchKeyStroke
private ConfigChangeListener configChangeListener
private ImmutableList<Node> modifiedSubtrees
private ProofTreeSearchBar proofTreeSearchPanel
public final TacletInfoToggle tacletInfoToggle
public ProofTreeView(KeYMediator mediator)
protected void finalize() throws Throwable
private void setProofTreeFont()
protected void layoutKeYComponent()
public KeYMediator mediator()
private void setMediator(KeYMediator m)
private void register()
private void unregister()
public void removeNotify()
removeNotify
in class 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(TreePath path)
protected void collapseOthers(TreePath path)
void selectBranchNode(GUIBranchNode node)
private void addModifiedNode(Node p_node)
public void showSearchPanel()