de.uka.ilkd.key.gui.prooftree

Class ProofTreeView.ProofTreePopupMenu

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JPopupMenu

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

All Implemented Interfaces:

java.awt.event.ActionListener, java.awt.event.ItemListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener, javax.accessibility.Accessible, javax.swing.MenuElement

Enclosing class:

ProofTreeView

class ProofTreeView.ProofTreePopupMenu
extends javax.swing.JPopupMenu
implements java.awt.event.ActionListener, java.awt.event.ItemListener

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	ProofTreeView.ProofTreePopupMenu.SetGoalsBelowEnableStatus Action for enabling/disabling all goals below "node".

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

javax.swing.JPopupMenu.AccessibleJPopupMenu, javax.swing.JPopupMenu.Separator

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
private javax.swing.tree.TreePath	branch
private javax.swing.JMenuItem	collapseAll
private javax.swing.JMenuItem	collapseBelow
private javax.swing.JMenuItem	collapseOtherBranches
private javax.swing.JMenuItem	delayedCut
private javax.swing.JMenuItem	expandAll
private javax.swing.JMenuItem	expandAllBelow
private javax.swing.JMenuItem	expandGoals
private javax.swing.JMenuItem	expandGoalsBelow
private java.util.Map<javax.swing.JCheckBoxMenuItem,ProofTreeViewFilter>	filters
private static int	ICON_SIZE
private Node	invokedNode
private javax.swing.JMenuItem	nextSibling
private javax.swing.JMenuItem	notes
private javax.swing.tree.TreePath	path
private javax.swing.JMenuItem	prevSibling
private javax.swing.JMenuItem	prune
private javax.swing.JMenuItem	runStrategy
private javax.swing.JMenuItem	search
private static long	serialVersionUID
private javax.swing.JMenuItem	subtreeStatistics

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
ProofTreePopupMenu(javax.swing.tree.TreePath p)

Method Summary

Modifier and Type	Method and Description
void	actionPerformed(java.awt.event.ActionEvent e)
private void	collapseBelow()
private void	create()
private void	expandGoalsBelow()
void	itemStateChanged(java.awt.event.ItemEvent e)
private void	openNotes()
private void	runStrategyOnNode() run automatic on the currently selected node.
private void	showSubtreeStatistics()

Methods inherited from class javax.swing.JPopupMenu

add, add, add, addMenuKeyListener, addPopupMenuListener, addSeparator, createActionChangeListener, createActionComponent, firePopupMenuCanceled, firePopupMenuWillBecomeInvisible, firePopupMenuWillBecomeVisible, getAccessibleContext, getComponent, getComponentAtIndex, getComponentIndex, getDefaultLightWeightPopupEnabled, getInvoker, getLabel, getMargin, getMenuKeyListeners, getPopupMenuListeners, getSelectionModel, getSubElements, getUI, getUIClassID, insert, insert, isBorderPainted, isLightWeightPopupEnabled, isPopupTrigger, isVisible, menuSelectionChanged, pack, paintBorder, paramString, processFocusEvent, processKeyEvent, processKeyEvent, processMouseEvent, remove, removeMenuKeyListener, removePopupMenuListener, setBorderPainted, setDefaultLightWeightPopupEnabled, setInvoker, setLabel, setLightWeightPopupEnabled, setLocation, setPopupSize, setPopupSize, setSelected, setSelectionModel, setUI, setVisible, show, 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, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, 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, 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, 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, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, 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, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle

Methods inherited from class java.lang.Object

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

Field Detail

ICON_SIZE

private static final int ICON_SIZE

See Also:

Constant Field Values

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

expandAll

private javax.swing.JMenuItem expandAll

expandAllBelow

private javax.swing.JMenuItem expandAllBelow

expandGoals

private javax.swing.JMenuItem expandGoals

expandGoalsBelow

private javax.swing.JMenuItem expandGoalsBelow

collapseAll

private javax.swing.JMenuItem collapseAll

collapseOtherBranches

private javax.swing.JMenuItem collapseOtherBranches

collapseBelow

private javax.swing.JMenuItem collapseBelow

prevSibling

private javax.swing.JMenuItem prevSibling

nextSibling

private javax.swing.JMenuItem nextSibling

filters

private java.util.Map<javax.swing.JCheckBoxMenuItem,ProofTreeViewFilter> filters

notes

private javax.swing.JMenuItem notes

search

private javax.swing.JMenuItem search

prune

private javax.swing.JMenuItem prune

delayedCut

private javax.swing.JMenuItem delayedCut

runStrategy

private javax.swing.JMenuItem runStrategy

subtreeStatistics

private javax.swing.JMenuItem subtreeStatistics

path

private javax.swing.tree.TreePath path

branch

private javax.swing.tree.TreePath branch

invokedNode

private Node invokedNode

Constructor Detail

ProofTreePopupMenu

public ProofTreePopupMenu(javax.swing.tree.TreePath p)

Method Detail

create

private void create()

actionPerformed

public void actionPerformed(java.awt.event.ActionEvent e)

Specified by:

actionPerformed in interface java.awt.event.ActionListener

openNotes

private void openNotes()

collapseBelow

private void collapseBelow()

expandGoalsBelow

private void expandGoalsBelow()

runStrategyOnNode

private void runStrategyOnNode()

run automatic on the currently selected node. All enabled goals below the current node are taken into consideration.

CAUTION: If the node itself is a goal then allow applying rules to it even if it were disabled. Desired behaviour?

showSubtreeStatistics

private void showSubtreeStatistics()

itemStateChanged

public void itemStateChanged(java.awt.event.ItemEvent e)

Specified by:

itemStateChanged in interface java.awt.event.ItemListener