de.uka.ilkd.key.gui.nodeviews

Class TacletMenu

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.AbstractButton

javax.swing.JMenuItem

javax.swing.JMenu

de.uka.ilkd.key.gui.nodeviews.TacletMenu

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.ItemSelectable, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible, javax.swing.MenuElement, javax.swing.SwingConstants

public class TacletMenu
extends javax.swing.JMenu

This class creates a menu with Taclets as entries. The invoker has to be of type SequentView because of the method call selectedTaclet that hands over the selected Taclet. The class is used to get all Taclet that are applicable at a selected position in a sequent.

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	TacletMenu.FocussedRuleApplicationMenuItem
(package private) class	TacletMenu.MenuControl ActionListener
static class	TacletMenu.TacletAppComparator

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

javax.swing.JMenu.AccessibleJMenu, javax.swing.JMenu.WinListener

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

javax.swing.JMenuItem.AccessibleJMenuItem

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

javax.swing.AbstractButton.AccessibleAbstractButton, javax.swing.AbstractButton.ButtonChangeListener

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 static java.lang.String	APPLY_CONTRACT
private static java.lang.String	APPLY_RULE
private static java.lang.String	CHANGE_ABBREVIATION
private static java.lang.String	CHOOSE_AND_APPLY_CONTRACT
private static java.util.Set<Name>	CLUTTER_RULES
private static java.util.Set<Name>	CLUTTER_RULESETS
private TacletMenu.TacletAppComparator	comp
private static java.lang.String	COPY_TO_CLIPBOARD
private static java.lang.String	CREATE_ABBREVIATION
private static java.lang.String	DISABLE_ABBREVIATION
private static java.lang.String	ENABLE_ABBREVIATION
private static java.lang.String	ENTER_LOOP_SPECIFICATION
private KeYMediator	mediator
private static java.lang.String	MORE_RULES
private static java.lang.String	NO_RULES_APPLICABLE
private PosInSequent	pos
private CurrentGoalView	sequentView
private static long	serialVersionUID

Fields inherited from class javax.swing.JMenu

popupListener

Fields inherited from class javax.swing.AbstractButton

actionListener, BORDER_PAINTED_CHANGED_PROPERTY, changeEvent, changeListener, CONTENT_AREA_FILLED_CHANGED_PROPERTY, DISABLED_ICON_CHANGED_PROPERTY, DISABLED_SELECTED_ICON_CHANGED_PROPERTY, FOCUS_PAINTED_CHANGED_PROPERTY, HORIZONTAL_ALIGNMENT_CHANGED_PROPERTY, HORIZONTAL_TEXT_POSITION_CHANGED_PROPERTY, ICON_CHANGED_PROPERTY, itemListener, MARGIN_CHANGED_PROPERTY, MNEMONIC_CHANGED_PROPERTY, model, MODEL_CHANGED_PROPERTY, PRESSED_ICON_CHANGED_PROPERTY, ROLLOVER_ENABLED_CHANGED_PROPERTY, ROLLOVER_ICON_CHANGED_PROPERTY, ROLLOVER_SELECTED_ICON_CHANGED_PROPERTY, SELECTED_ICON_CHANGED_PROPERTY, TEXT_CHANGED_PROPERTY, VERTICAL_ALIGNMENT_CHANGED_PROPERTY, VERTICAL_TEXT_POSITION_CHANGED_PROPERTY

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 javax.swing.SwingConstants

BOTTOM, CENTER, EAST, HORIZONTAL, LEADING, LEFT, NEXT, NORTH, NORTH_EAST, NORTH_WEST, PREVIOUS, RIGHT, SOUTH, SOUTH_EAST, SOUTH_WEST, TOP, TRAILING, VERTICAL, WEST

Fields inherited from interface java.awt.image.ImageObserver

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

Constructor Summary

Constructors

Constructor and Description
TacletMenu() creates empty menu
TacletMenu(CurrentGoalView sequentView, ImmutableList<TacletApp> findList, ImmutableList<TacletApp> rewriteList, ImmutableList<TacletApp> noFindList, ImmutableList<BuiltInRule> builtInList, PosInSequent pos) creates a new menu that displays all applicable rules at the given position

Method Summary

Modifier and Type	Method and Description
private void	addBuiltInRuleItem(BuiltInRule builtInRule, TacletMenu.MenuControl control) adds an item for built in rules (e.g.
private void	addClipboardItem(TacletMenu.MenuControl control)
private void	addMacroMenu()
private void	createAbbrevSection(Term t, TacletMenu.MenuControl control)
private void	createBuiltInRuleMenu(ImmutableList<BuiltInRule> builtInList, TacletMenu.MenuControl control)
private void	createDelayedCutJoinMenu(TacletMenu.MenuControl control)
private void	createFocussedAutoModeMenu(TacletMenu.MenuControl control)
private void	createMenuItems(ImmutableList<TacletApp> taclets, TacletMenu.MenuControl control) adds a TacletMenuItem for each taclet in the list and sets the given MenuControl as the ActionListener
private void	createMergeRuleMenu() Creates the menu item for the "defocusing" merge rule which links partner nodes to merge nodes.
private void	createNameCreationInfoSection(TacletMenu.MenuControl control)
private void	createSection(java.lang.String title) inserts separator followed from the section's title
private void	createSMTMenu(TacletMenu.MenuControl control)
private void	createTacletMenu(ImmutableList<TacletApp> find, ImmutableList<TacletApp> noFind, ImmutableList<BuiltInRule> builtInList, TacletMenu.MenuControl control) creates the menu by adding all sub-menus and items
(package private) void	invisible() makes submenus invisible
static ImmutableList<TacletApp>	removeRewrites(ImmutableList<TacletApp> list) removes RewriteTaclet from list
static ImmutableList<TacletApp>	sort(ImmutableList<TacletApp> finds, TacletMenu.TacletAppComparator comp) This method is also used by the KeYIDE has to be static and public.

Methods inherited from class javax.swing.JMenu

add, add, add, add, add, addMenuListener, addSeparator, applyComponentOrientation, createActionChangeListener, createActionComponent, createWinListener, doClick, fireMenuCanceled, fireMenuDeselected, fireMenuSelected, getAccessibleContext, getComponent, getDelay, getItem, getItemCount, getMenuComponent, getMenuComponentCount, getMenuComponents, getMenuListeners, getPopupMenu, getPopupMenuOrigin, getSubElements, getUIClassID, insert, insert, insert, insertSeparator, isMenuComponent, isPopupMenuVisible, isSelected, isTearOff, isTopLevelMenu, menuSelectionChanged, paramString, processKeyEvent, remove, remove, remove, removeAll, removeMenuListener, setAccelerator, setComponentOrientation, setDelay, setMenuLocation, setModel, setPopupMenuVisible, setSelected, updateUI

Methods inherited from class javax.swing.JMenuItem

actionPropertyChanged, addMenuDragMouseListener, addMenuKeyListener, configurePropertiesFromAction, fireMenuDragMouseDragged, fireMenuDragMouseEntered, fireMenuDragMouseExited, fireMenuDragMouseReleased, fireMenuKeyPressed, fireMenuKeyReleased, fireMenuKeyTyped, getAccelerator, getMenuDragMouseListeners, getMenuKeyListeners, init, isArmed, processKeyEvent, processMenuDragMouseEvent, processMenuKeyEvent, processMouseEvent, removeMenuDragMouseListener, removeMenuKeyListener, setArmed, setEnabled, setUI

Methods inherited from class javax.swing.AbstractButton

addActionListener, addChangeListener, addImpl, addItemListener, checkHorizontalKey, checkVerticalKey, createActionListener, createActionPropertyChangeListener, createChangeListener, createItemListener, doClick, fireActionPerformed, fireItemStateChanged, fireStateChanged, getAction, getActionCommand, getActionListeners, getChangeListeners, getDisabledIcon, getDisabledSelectedIcon, getDisplayedMnemonicIndex, getHideActionText, getHorizontalAlignment, getHorizontalTextPosition, getIcon, getIconTextGap, getItemListeners, getLabel, getMargin, getMnemonic, getModel, getMultiClickThreshhold, getPressedIcon, getRolloverIcon, getRolloverSelectedIcon, getSelectedIcon, getSelectedObjects, getText, getUI, getVerticalAlignment, getVerticalTextPosition, imageUpdate, isBorderPainted, isContentAreaFilled, isFocusPainted, isRolloverEnabled, paintBorder, removeActionListener, removeChangeListener, removeItemListener, removeNotify, setAction, setActionCommand, setBorderPainted, setContentAreaFilled, setDisabledIcon, setDisabledSelectedIcon, setDisplayedMnemonicIndex, setFocusPainted, setHideActionText, setHorizontalAlignment, setHorizontalTextPosition, setIcon, setIconTextGap, setLabel, setLayout, setMargin, setMnemonic, setMnemonic, setMultiClickThreshhold, setPressedIcon, setRolloverEnabled, setRolloverIcon, setRolloverSelectedIcon, setSelectedIcon, setText, setUI, setVerticalAlignment, setVerticalTextPosition

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, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, 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, addContainerListener, addPropertyChangeListener, addPropertyChangeListener, 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, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, 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, 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, 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, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface javax.swing.MenuElement

processKeyEvent, processMouseEvent

Field Detail

MORE_RULES

private static final java.lang.String MORE_RULES

See Also:

Constant Field Values

COPY_TO_CLIPBOARD

private static final java.lang.String COPY_TO_CLIPBOARD

See Also:

Constant Field Values

CREATE_ABBREVIATION

private static final java.lang.String CREATE_ABBREVIATION

See Also:

Constant Field Values

ENABLE_ABBREVIATION

private static final java.lang.String ENABLE_ABBREVIATION

See Also:

Constant Field Values

DISABLE_ABBREVIATION

private static final java.lang.String DISABLE_ABBREVIATION

See Also:

Constant Field Values

CHANGE_ABBREVIATION

private static final java.lang.String CHANGE_ABBREVIATION

See Also:

Constant Field Values

APPLY_CONTRACT

private static final java.lang.String APPLY_CONTRACT

See Also:

Constant Field Values

CHOOSE_AND_APPLY_CONTRACT

private static final java.lang.String CHOOSE_AND_APPLY_CONTRACT

See Also:

Constant Field Values

ENTER_LOOP_SPECIFICATION

private static final java.lang.String ENTER_LOOP_SPECIFICATION

See Also:

Constant Field Values

APPLY_RULE

private static final java.lang.String APPLY_RULE

See Also:

Constant Field Values

NO_RULES_APPLICABLE

private static final java.lang.String NO_RULES_APPLICABLE

See Also:

Constant Field Values

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

pos

private PosInSequent pos

sequentView

private CurrentGoalView sequentView

mediator

private KeYMediator mediator

CLUTTER_RULESETS

private static final java.util.Set<Name> CLUTTER_RULESETS

CLUTTER_RULES

private static final java.util.Set<Name> CLUTTER_RULES

comp

private TacletMenu.TacletAppComparator comp

Constructor Detail

TacletMenu

TacletMenu()

creates empty menu

TacletMenu

TacletMenu(CurrentGoalView sequentView,
           ImmutableList<TacletApp> findList,
           ImmutableList<TacletApp> rewriteList,
           ImmutableList<TacletApp> noFindList,
           ImmutableList<BuiltInRule> builtInList,
           PosInSequent pos)

creates a new menu that displays all applicable rules at the given position

Parameters:

sequentView - the SequentView that is the parent of this menu

findList - IList with all applicable FindTaclets

rewriteList - IList with all applicable RewriteTaclets

noFindList - IList with all applicable noFindTaclets

builtInList - IList with all applicable BuiltInRules

pos - the PosInSequent

Method Detail

removeRewrites

public static ImmutableList<TacletApp> removeRewrites(ImmutableList<TacletApp> list)

removes RewriteTaclet from list

Parameters:

list - the IList from where the RewriteTaclet are removed

Returns:

list without RewriteTaclets

createTacletMenu

private void createTacletMenu(ImmutableList<TacletApp> find,
                              ImmutableList<TacletApp> noFind,
                              ImmutableList<BuiltInRule> builtInList,
                              TacletMenu.MenuControl control)

creates the menu by adding all sub-menus and items

createBuiltInRuleMenu

private void createBuiltInRuleMenu(ImmutableList<BuiltInRule> builtInList,
                                   TacletMenu.MenuControl control)

addMacroMenu

private void addMacroMenu()

createSMTMenu

private void createSMTMenu(TacletMenu.MenuControl control)

createDelayedCutJoinMenu

private void createDelayedCutJoinMenu(TacletMenu.MenuControl control)

createMergeRuleMenu

private void createMergeRuleMenu()

Creates the menu item for the "defocusing" merge rule which links partner nodes to merge nodes.

addBuiltInRuleItem

private void addBuiltInRuleItem(BuiltInRule builtInRule,
                                TacletMenu.MenuControl control)

adds an item for built in rules (e.g. Run Simplify or Update Simplifier)

createFocussedAutoModeMenu

private void createFocussedAutoModeMenu(TacletMenu.MenuControl control)

sort

public static ImmutableList<TacletApp> sort(ImmutableList<TacletApp> finds,
                                            TacletMenu.TacletAppComparator comp)

This method is also used by the KeYIDE has to be static and public.

createAbbrevSection

private void createAbbrevSection(Term t,
                                 TacletMenu.MenuControl control)

createNameCreationInfoSection

private void createNameCreationInfoSection(TacletMenu.MenuControl control)

createSection

private void createSection(java.lang.String title)

inserts separator followed from the section's title

Parameters:

title - a String that contains the title of the section

addClipboardItem

private void addClipboardItem(TacletMenu.MenuControl control)

createMenuItems

private void createMenuItems(ImmutableList<TacletApp> taclets,
                             TacletMenu.MenuControl control)

adds a TacletMenuItem for each taclet in the list and sets the given MenuControl as the ActionListener

Parameters:

taclets - IList with the Taclets the items represent

control - the ActionListener

invisible

void invisible()

makes submenus invisible