public class TacletMenu extends JMenu
Modifier and Type | Class and Description |
---|---|
(package private) static class |
TacletMenu.FocussedRuleApplicationMenuItem |
(package private) class |
TacletMenu.MenuControl
ActionListener
|
static class |
TacletMenu.TacletAppComparator |
JMenu.AccessibleJMenu, JMenu.WinListener
JMenuItem.AccessibleJMenuItem
AbstractButton.AccessibleAbstractButton, AbstractButton.ButtonChangeListener
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
private static String |
APPLY_CONTRACT |
private static String |
APPLY_RULE |
private static String |
CHANGE_ABBREVIATION |
private static String |
CHOOSE_AND_APPLY_CONTRACT |
private static Set<Name> |
CLUTTER_RULES |
private static Set<Name> |
CLUTTER_RULESETS |
private TacletMenu.TacletAppComparator |
comp |
private static String |
COPY_TO_CLIPBOARD |
private static String |
CREATE_ABBREVIATION |
private static String |
DISABLE_ABBREVIATION |
private static String |
ENABLE_ABBREVIATION |
private static String |
ENTER_LOOP_SPECIFICATION |
private KeYMediator |
mediator |
private static String |
MORE_RULES |
private static String |
NO_RULES_APPLICABLE |
private PosInSequent |
pos |
private CurrentGoalView |
sequentView |
private static long |
serialVersionUID |
popupListener
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
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
BOTTOM, CENTER, EAST, HORIZONTAL, LEADING, LEFT, NEXT, NORTH, NORTH_EAST, NORTH_WEST, PREVIOUS, RIGHT, SOUTH, SOUTH_EAST, SOUTH_WEST, TOP, TRAILING, VERTICAL, WEST
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
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
|
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 |
createDefocusingJoinMenu()
Creates the menu item for the "defocusing" join rule which links partner
nodes to join nodes.
|
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 |
createNameCreationInfoSection(TacletMenu.MenuControl control) |
private void |
createSection(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.
|
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
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
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
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
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
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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
processKeyEvent, processMouseEvent
private static final String MORE_RULES
private static final String COPY_TO_CLIPBOARD
private static final String CREATE_ABBREVIATION
private static final String ENABLE_ABBREVIATION
private static final String DISABLE_ABBREVIATION
private static final String CHANGE_ABBREVIATION
private static final String APPLY_CONTRACT
private static final String CHOOSE_AND_APPLY_CONTRACT
private static final String ENTER_LOOP_SPECIFICATION
private static final String APPLY_RULE
private static final String NO_RULES_APPLICABLE
private static final long serialVersionUID
private PosInSequent pos
private CurrentGoalView sequentView
private KeYMediator mediator
private TacletMenu.TacletAppComparator comp
TacletMenu()
TacletMenu(CurrentGoalView sequentView, ImmutableList<TacletApp> findList, ImmutableList<TacletApp> rewriteList, ImmutableList<TacletApp> noFindList, ImmutableList<BuiltInRule> builtInList, PosInSequent pos)
sequentView
- the SequentView that is the parent of this menufindList
- IListrewriteList
- IListnoFindList
- IListbuiltInList
- IListpos
- the PosInSequentpublic static ImmutableList<TacletApp> removeRewrites(ImmutableList<TacletApp> list)
list
- the IListprivate void createTacletMenu(ImmutableList<TacletApp> find, ImmutableList<TacletApp> noFind, ImmutableList<BuiltInRule> builtInList, TacletMenu.MenuControl control)
private void createBuiltInRuleMenu(ImmutableList<BuiltInRule> builtInList, TacletMenu.MenuControl control)
private void addMacroMenu()
private void createSMTMenu(TacletMenu.MenuControl control)
private void createDelayedCutJoinMenu(TacletMenu.MenuControl control)
private void createDefocusingJoinMenu()
private void addBuiltInRuleItem(BuiltInRule builtInRule, TacletMenu.MenuControl control)
private void createFocussedAutoModeMenu(TacletMenu.MenuControl control)
public static ImmutableList<TacletApp> sort(ImmutableList<TacletApp> finds, TacletMenu.TacletAppComparator comp)
private void createAbbrevSection(Term t, TacletMenu.MenuControl control)
private void createNameCreationInfoSection(TacletMenu.MenuControl control)
private void createSection(String title)
title
- a String that contains the title of the sectionprivate void addClipboardItem(TacletMenu.MenuControl control)
private void createMenuItems(ImmutableList<TacletApp> taclets, TacletMenu.MenuControl control)
taclets
- IListcontrol
- the ActionListenervoid invisible()