public class TacletMenu
extends javax.swing.JMenu
Modifier and Type | Class and Description |
---|---|
(package private) static class |
TacletMenu.FocussedRuleApplicationMenuItem |
(package private) class |
TacletMenu.MenuControl
ActionListener
|
static class |
TacletMenu.TacletAppComparator |
javax.swing.JMenu.AccessibleJMenu, javax.swing.JMenu.WinListener
javax.swing.JMenuItem.AccessibleJMenuItem
javax.swing.AbstractButton.AccessibleAbstractButton, javax.swing.AbstractButton.ButtonChangeListener
javax.swing.JComponent.AccessibleJComponent
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 |
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
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
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 |
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.
|
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
private static final java.lang.String MORE_RULES
private static final java.lang.String COPY_TO_CLIPBOARD
private static final java.lang.String CREATE_ABBREVIATION
private static final java.lang.String ENABLE_ABBREVIATION
private static final java.lang.String DISABLE_ABBREVIATION
private static final java.lang.String CHANGE_ABBREVIATION
private static final java.lang.String APPLY_CONTRACT
private static final java.lang.String CHOOSE_AND_APPLY_CONTRACT
private static final java.lang.String ENTER_LOOP_SPECIFICATION
private static final java.lang.String APPLY_RULE
private static final java.lang.String NO_RULES_APPLICABLE
private static final long serialVersionUID
private PosInSequent pos
private CurrentGoalView sequentView
private KeYMediator mediator
private static final java.util.Set<Name> CLUTTER_RULESETS
private static final java.util.Set<Name> CLUTTER_RULES
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
- IList
with all applicable FindTacletsrewriteList
- IList
with all applicable RewriteTacletsnoFindList
- IList
with all applicable noFindTacletsbuiltInList
- IList
with all applicable BuiltInRulespos
- the PosInSequentpublic static ImmutableList<TacletApp> removeRewrites(ImmutableList<TacletApp> list)
list
- the IList
from where the RewriteTaclet are
removedprivate 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 createMergeRuleMenu()
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(java.lang.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
- IList
with the Taclets the items representcontrol
- the ActionListenervoid invisible()