public abstract class InsertionTacletBrowserMenuItem
extends javax.swing.JMenu
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 |
---|---|
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
|
protected Services |
services
the services
|
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
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 |
---|
InsertionTacletBrowserMenuItem(java.lang.String title,
javax.swing.JFrame parent,
NotationInfo notInfo,
Services services) |
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()
gets the Taclet that is attached to this item
|
protected java.util.Collection<de.uka.ilkd.key.gui.nodeviews.InsertionTacletBrowserMenuItem.TacletAppListItem> |
createInsertionList() |
de.uka.ilkd.key.gui.nodeviews.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) |
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
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
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
protected NotationInfo notInfo
protected javax.swing.JFrame parent
protected Services services
public InsertionTacletBrowserMenuItem(java.lang.String title, javax.swing.JFrame parent, NotationInfo notInfo, Services services)
protected java.util.Collection<de.uka.ilkd.key.gui.nodeviews.InsertionTacletBrowserMenuItem.TacletAppListItem> createInsertionList()
public void add(TacletApp app)
isResponsible(de.uka.ilkd.key.rule.Taclet)
.app
- the TacletApp to be addedpublic void addActionListener(java.awt.event.ActionListener listener)
addActionListener
in class javax.swing.AbstractButton
public TacletApp connectedTo()
public int getAppSize()
public boolean isResponsible(Taclet t)
t
- the Taclet to be checkedpublic void openDialog()
protected void processTacletSelected(java.awt.event.ActionEvent e)
public void removeActionListener(java.awt.event.ActionListener listener)
removeActionListener
in class javax.swing.AbstractButton
public de.uka.ilkd.key.gui.nodeviews.InsertionTacletBrowserMenuItem.TacletAppListItem createListItem(TacletApp app)
Copyright © 2003-2019 The KeY-Project.