de.uka.ilkd.key.gui.nodeviews

Class MenuItemForTwoModeRules

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.MenuItemForTwoModeRules

All Implemented Interfaces:

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

public class MenuItemForTwoModeRules
extends javax.swing.JMenu
implements BuiltInRuleMenuItem

See Also:

Serialized Form

Nested Class Summary

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 boolean	DEFAULT_FORCE
private static int	EXPAND_DELAY
private boolean	forcedMode
private java.awt.event.ActionListener	listener
private BuiltInRule	rule
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
MenuItemForTwoModeRules(java.lang.String mainName, java.lang.String actionTextForForcedMode, java.lang.String tooltipForcedMode, java.lang.String actionTextForInteractiveMode, java.lang.String tooltipInteractiveMode, BuiltInRule rule)

Method Summary

Modifier and Type	Method and Description
void	addActionListener(java.awt.event.ActionListener al)
BuiltInRule	connectedTo()
boolean	forcedApplication()
private void	init(java.lang.String actionTextForForcedMode, java.lang.String tooltipForcedMode, java.lang.String actionTextForInteractiveMode, java.lang.String tooltipInteractiveMode)
void	removeActionListener(java.awt.event.ActionListener al)

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

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, 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

EXPAND_DELAY

private static final int EXPAND_DELAY

See Also:

Constant Field Values

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

DEFAULT_FORCE

private static final boolean DEFAULT_FORCE

See Also:

Constant Field Values

rule

private final BuiltInRule rule

forcedMode

private boolean forcedMode

listener

private java.awt.event.ActionListener listener

Constructor Detail

MenuItemForTwoModeRules

public MenuItemForTwoModeRules(java.lang.String mainName,
                               java.lang.String actionTextForForcedMode,
                               java.lang.String tooltipForcedMode,
                               java.lang.String actionTextForInteractiveMode,
                               java.lang.String tooltipInteractiveMode,
                               BuiltInRule rule)

Method Detail

init

private void init(java.lang.String actionTextForForcedMode,
                  java.lang.String tooltipForcedMode,
                  java.lang.String actionTextForInteractiveMode,
                  java.lang.String tooltipInteractiveMode)

addActionListener

public void addActionListener(java.awt.event.ActionListener al)

Overrides:

addActionListener in class javax.swing.AbstractButton

removeActionListener

public void removeActionListener(java.awt.event.ActionListener al)

Overrides:

removeActionListener in class javax.swing.AbstractButton

connectedTo

public BuiltInRule connectedTo()

Specified by:

connectedTo in interface BuiltInRuleMenuItem

forcedApplication

public boolean forcedApplication()

Specified by:

forcedApplication in interface BuiltInRuleMenuItem