de.uka.ilkd.key.gui.nodeviews

Class InsertionTacletBrowserMenuItem

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

All Implemented Interfaces:

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

Direct Known Subclasses:

InsertHiddenTacletMenuItem, InsertSystemInvariantTacletMenuItem

public abstract class InsertionTacletBrowserMenuItem
extends javax.swing.JMenu
implements TacletMenuItem

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	InsertionTacletBrowserMenuItem.TacletAppListItem inner class to pretty print the formulas to be added

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 java.lang.String	baseTitle the base title; used title = basetitle + ( nrOfItems )
private java.util.Collection<InsertionTacletBrowserMenuItem.TacletAppListItem>	insertionTaclets all taclet apps the user can choose from
private java.util.List<java.awt.event.ActionListener>	listenerList the added action listeners
private static int	MAX_ITEM_NUMBER The number of items that are to be shown in the dialog before a message referring to the dialog is issued.
protected NotationInfo	notInfo the notation info to pretty print the taclet apps
protected javax.swing.JFrame	parent the parent frame of the selection dialog to be displayed
private TacletApp	selectedTaclet the selected taclet to be applied
private static long	serialVersionUID
protected Services	services the services

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

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
InsertionTacletBrowserMenuItem(java.lang.String title, javax.swing.JFrame parent, NotationInfo notInfo, Services services)

Method Summary

Modifier and Type	Method and Description
void	add(TacletApp app) adds a new taclet to be displayed by this component it is assumed that the app has been tested before by isResponsible(de.uka.ilkd.key.rule.Taclet)
void	addActionListener(java.awt.event.ActionListener listener)
protected abstract Sequent	checkTaclet(Taclet t)
TacletApp	connectedTo() returns the selected taclet to be applied
protected java.util.Collection<InsertionTacletBrowserMenuItem.TacletAppListItem>	createInsertionList() returns the list where the tacletappItems are stored (allows easy exchange for e.g. a sorted list) default: is filo
InsertionTacletBrowserMenuItem.TacletAppListItem	createListItem(TacletApp app)
int	getAppSize()
boolean	isResponsible(Taclet t) tests if this class is responsible for the given taclet
void	openDialog() opens the selection dialog displaying all hidden formulas in a list and allowing the user to select the one to be added
protected void	processTacletSelected(java.awt.event.ActionEvent e)
void	removeActionListener(java.awt.event.ActionListener listener)

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

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

MAX_ITEM_NUMBER

private static final int MAX_ITEM_NUMBER

The number of items that are to be shown in the dialog before a message referring to the dialog is issued. There are always "Open Dialog" and a JSeparator"

See Also:

Constant Field Values

insertionTaclets

private java.util.Collection<InsertionTacletBrowserMenuItem.TacletAppListItem> insertionTaclets

all taclet apps the user can choose from

listenerList

private java.util.List<java.awt.event.ActionListener> listenerList

the added action listeners

notInfo

protected NotationInfo notInfo

the notation info to pretty print the taclet apps

parent

protected javax.swing.JFrame parent

the parent frame of the selection dialog to be displayed

selectedTaclet

private TacletApp selectedTaclet

the selected taclet to be applied

services

protected Services services

the services

baseTitle

private java.lang.String baseTitle

the base title; used title = basetitle + ( nrOfItems )

Constructor Detail

InsertionTacletBrowserMenuItem

public InsertionTacletBrowserMenuItem(java.lang.String title,
                                      javax.swing.JFrame parent,
                                      NotationInfo notInfo,
                                      Services services)

Method Detail

createInsertionList

protected java.util.Collection<InsertionTacletBrowserMenuItem.TacletAppListItem> createInsertionList()

returns the list where the tacletappItems are stored (allows easy exchange for e.g. a sorted list) default: is filo

add

public void add(TacletApp app)

adds a new taclet to be displayed by this component it is assumed that the app has been tested before by isResponsible(de.uka.ilkd.key.rule.Taclet)

Parameters:

app - the TacletApp to be added

addActionListener

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

Specified by:

addActionListener in interface TacletMenuItem

Overrides:

addActionListener in class javax.swing.AbstractButton

checkTaclet

protected abstract Sequent checkTaclet(Taclet t)

connectedTo

public TacletApp connectedTo()

returns the selected taclet to be applied

Specified by:

connectedTo in interface TacletMenuItem

Returns:

the attached Taclet

getAppSize

public int getAppSize()

isResponsible

public boolean isResponsible(Taclet t)

tests if this class is responsible for the given taclet

Parameters:

t - the Taclet to be checked

Returns:

true if this item implementation shall be used

openDialog

public void openDialog()

opens the selection dialog displaying all hidden formulas in a list and allowing the user to select the one to be added

processTacletSelected

protected void processTacletSelected(java.awt.event.ActionEvent e)

removeActionListener

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

Overrides:

removeActionListener in class javax.swing.AbstractButton

createListItem

public InsertionTacletBrowserMenuItem.TacletAppListItem createListItem(TacletApp app)