| |
|
| javax.swing.JComponent javax.swing.AbstractButton javax.swing.JMenuItem javax.swing.JMenu de.uka.ilkd.key.gui.nodeviews.TacletMenu
TacletMenu | class TacletMenu extends JMenu (Code) | | This class creates a menu with Taclets as entries. The invoker has
to be of type SequentView because of the method call selectedTaclet
that hands over the selected Taclet. The class is used to get all
Taclet that are applicable at a selected position in a sequent.
|
Inner Class :static class FocussedRuleApplicationMenuItem extends JMenuItem | |
Inner Class :static class TacletAppComparator implements Comparator | |
Field Summary | |
static Logger | logger |
logger | static Logger logger(Code) | | |
TacletMenu | TacletMenu()(Code) | | creates empty menu
|
TacletMenu | TacletMenu(SequentView sequentView, ListOfTacletApp findList, ListOfTacletApp rewriteList, ListOfTacletApp noFindList, ListOfBuiltInRule builtInList, PosInSequent pos)(Code) | | creates a new menu that displays all applicable rules at the given
position
Parameters: sequentView - the SequentView that is the parent of this menu Parameters: findList - ListOfTaclet with all applicable FindTaclets Parameters: rewriteList - ListOfTaclet with all applicable RewriteTaclets Parameters: noFindList - ListOfTaclet with all applicable noFindTaclets Parameters: builtInList - ListOfBuiltInRule with all applicable BuiltInRules Parameters: pos - the PosInSequent |
invisible | void invisible()(Code) | | makes submenus invisible
|
Fields inherited from javax.swing.JMenu | protected WinListener popupListener(Code)(Java Doc)
|
Methods inherited from javax.swing.AbstractButton | protected void actionPropertyChanged(Action action, String propertyName)(Code)(Java Doc) public void addActionListener(ActionListener l)(Code)(Java Doc) public void addChangeListener(ChangeListener l)(Code)(Java Doc) protected void addImpl(Component comp, Object constraints, int index)(Code)(Java Doc) public void addItemListener(ItemListener l)(Code)(Java Doc) protected int checkHorizontalKey(int key, String exception)(Code)(Java Doc) protected int checkVerticalKey(int key, String exception)(Code)(Java Doc) protected void configurePropertiesFromAction(Action a)(Code)(Java Doc) protected ActionListener createActionListener()(Code)(Java Doc) protected PropertyChangeListener createActionPropertyChangeListener(Action a)(Code)(Java Doc) protected ChangeListener createChangeListener()(Code)(Java Doc) protected ItemListener createItemListener()(Code)(Java Doc) public void doClick()(Code)(Java Doc) public void doClick(int pressTime)(Code)(Java Doc) protected void fireActionPerformed(ActionEvent event)(Code)(Java Doc) protected void fireItemStateChanged(ItemEvent event)(Code)(Java Doc) protected void fireStateChanged()(Code)(Java Doc) public Action getAction()(Code)(Java Doc) public String getActionCommand()(Code)(Java Doc) public ActionListener[] getActionListeners()(Code)(Java Doc) public ChangeListener[] getChangeListeners()(Code)(Java Doc) public Icon getDisabledIcon()(Code)(Java Doc) public Icon getDisabledSelectedIcon()(Code)(Java Doc) public int getDisplayedMnemonicIndex()(Code)(Java Doc) public boolean getHideActionText()(Code)(Java Doc) public int getHorizontalAlignment()(Code)(Java Doc) public int getHorizontalTextPosition()(Code)(Java Doc) public Icon getIcon()(Code)(Java Doc) public int getIconTextGap()(Code)(Java Doc) public ItemListener[] getItemListeners()(Code)(Java Doc) public String getLabel()(Code)(Java Doc) public Insets getMargin()(Code)(Java Doc) public int getMnemonic()(Code)(Java Doc) public ButtonModel getModel()(Code)(Java Doc) public long getMultiClickThreshhold()(Code)(Java Doc) public Icon getPressedIcon()(Code)(Java Doc) public Icon getRolloverIcon()(Code)(Java Doc) public Icon getRolloverSelectedIcon()(Code)(Java Doc) public Icon getSelectedIcon()(Code)(Java Doc) public Object[] getSelectedObjects()(Code)(Java Doc) public String getText()(Code)(Java Doc) public ButtonUI getUI()(Code)(Java Doc) public int getVerticalAlignment()(Code)(Java Doc) public int getVerticalTextPosition()(Code)(Java Doc) public boolean imageUpdate(Image img, int infoflags, int x, int y, int w, int h)(Code)(Java Doc) protected void init(String text, Icon icon)(Code)(Java Doc) public boolean isBorderPainted()(Code)(Java Doc) public boolean isContentAreaFilled()(Code)(Java Doc) public boolean isFocusPainted()(Code)(Java Doc) public boolean isRolloverEnabled()(Code)(Java Doc) public boolean isSelected()(Code)(Java Doc) protected void paintBorder(Graphics g)(Code)(Java Doc) protected String paramString()(Code)(Java Doc) public void removeActionListener(ActionListener l)(Code)(Java Doc) public void removeChangeListener(ChangeListener l)(Code)(Java Doc) public void removeItemListener(ItemListener l)(Code)(Java Doc) public void removeNotify()(Code)(Java Doc) public void setAction(Action a)(Code)(Java Doc) public void setActionCommand(String actionCommand)(Code)(Java Doc) public void setBorderPainted(boolean b)(Code)(Java Doc) public void setContentAreaFilled(boolean b)(Code)(Java Doc) public void setDisabledIcon(Icon disabledIcon)(Code)(Java Doc) public void setDisabledSelectedIcon(Icon disabledSelectedIcon)(Code)(Java Doc) public void setDisplayedMnemonicIndex(int index) throws IllegalArgumentException(Code)(Java Doc) public void setEnabled(boolean b)(Code)(Java Doc) public void setFocusPainted(boolean b)(Code)(Java Doc) public void setHideActionText(boolean hideActionText)(Code)(Java Doc) public void setHorizontalAlignment(int alignment)(Code)(Java Doc) public void setHorizontalTextPosition(int textPosition)(Code)(Java Doc) public void setIcon(Icon defaultIcon)(Code)(Java Doc) public void setIconTextGap(int iconTextGap)(Code)(Java Doc) public void setLabel(String label)(Code)(Java Doc) public void setLayout(LayoutManager mgr)(Code)(Java Doc) public void setMargin(Insets m)(Code)(Java Doc) public void setMnemonic(int mnemonic)(Code)(Java Doc) public void setMnemonic(char mnemonic)(Code)(Java Doc) public void setModel(ButtonModel newModel)(Code)(Java Doc) public void setMultiClickThreshhold(long threshhold)(Code)(Java Doc) public void setPressedIcon(Icon pressedIcon)(Code)(Java Doc) public void setRolloverEnabled(boolean b)(Code)(Java Doc) public void setRolloverIcon(Icon rolloverIcon)(Code)(Java Doc) public void setRolloverSelectedIcon(Icon rolloverSelectedIcon)(Code)(Java Doc) public void setSelected(boolean b)(Code)(Java Doc) public void setSelectedIcon(Icon selectedIcon)(Code)(Java Doc) public void setText(String text)(Code)(Java Doc) public void setUI(ButtonUI ui)(Code)(Java Doc) public void setVerticalAlignment(int alignment)(Code)(Java Doc) public void setVerticalTextPosition(int textPosition)(Code)(Java Doc) public void updateUI()(Code)(Java Doc)
|
Methods inherited from javax.swing.JComponent | public void addAncestorListener(AncestorListener listener)(Code)(Java Doc) public void addNotify()(Code)(Java Doc) public synchronized void addVetoableChangeListener(VetoableChangeListener listener)(Code)(Java Doc) public void computeVisibleRect(Rectangle visibleRect)(Code)(Java Doc) public boolean contains(int x, int y)(Code)(Java Doc) public JToolTip createToolTip()(Code)(Java Doc) public void disable()(Code)(Java Doc) public void enable()(Code)(Java Doc) public void firePropertyChange(String propertyName, boolean oldValue, boolean newValue)(Code)(Java Doc) public void firePropertyChange(String propertyName, int oldValue, int newValue)(Code)(Java Doc) public void firePropertyChange(String propertyName, char oldValue, char newValue)(Code)(Java Doc) protected void fireVetoableChange(String propertyName, Object oldValue, Object newValue) throws java.beans.PropertyVetoException(Code)(Java Doc) public AccessibleContext getAccessibleContext()(Code)(Java Doc) public ActionListener getActionForKeyStroke(KeyStroke aKeyStroke)(Code)(Java Doc) final public ActionMap getActionMap()(Code)(Java Doc) public float getAlignmentX()(Code)(Java Doc) public float getAlignmentY()(Code)(Java Doc) public AncestorListener[] getAncestorListeners()(Code)(Java Doc) public boolean getAutoscrolls()(Code)(Java Doc) public int getBaseline(int width, int height)(Code)(Java Doc) public BaselineResizeBehavior getBaselineResizeBehavior()(Code)(Java Doc) public Border getBorder()(Code)(Java Doc) public Rectangle getBounds(Rectangle rv)(Code)(Java Doc) final public Object getClientProperty(Object key)(Code)(Java Doc) protected Graphics getComponentGraphics(Graphics g)(Code)(Java Doc) public JPopupMenu getComponentPopupMenu()(Code)(Java Doc) public int getConditionForKeyStroke(KeyStroke aKeyStroke)(Code)(Java Doc) public int getDebugGraphicsOptions()(Code)(Java Doc) public static Locale getDefaultLocale()(Code)(Java Doc) public FontMetrics getFontMetrics(Font font)(Code)(Java Doc) public Graphics getGraphics()(Code)(Java Doc) public int getHeight()(Code)(Java Doc) public boolean getInheritsPopupMenu()(Code)(Java Doc) final public InputMap getInputMap(int condition)(Code)(Java Doc) final public InputMap getInputMap()(Code)(Java Doc) public InputVerifier getInputVerifier()(Code)(Java Doc) public Insets getInsets()(Code)(Java Doc) public Insets getInsets(Insets insets)(Code)(Java Doc) public T[] getListeners(Class<T> listenerType)(Code)(Java Doc) public Point getLocation(Point rv)(Code)(Java Doc) public Dimension getMaximumSize()(Code)(Java Doc) public Dimension getMinimumSize()(Code)(Java Doc) public Component getNextFocusableComponent()(Code)(Java Doc) public Point getPopupLocation(MouseEvent event)(Code)(Java Doc) public Dimension getPreferredSize()(Code)(Java Doc) public KeyStroke[] getRegisteredKeyStrokes()(Code)(Java Doc) public JRootPane getRootPane()(Code)(Java Doc) public Dimension getSize(Dimension rv)(Code)(Java Doc) public Point getToolTipLocation(MouseEvent event)(Code)(Java Doc) public String getToolTipText()(Code)(Java Doc) public String getToolTipText(MouseEvent event)(Code)(Java Doc) public Container getTopLevelAncestor()(Code)(Java Doc) public TransferHandler getTransferHandler()(Code)(Java Doc) public String getUIClassID()(Code)(Java Doc) public boolean getVerifyInputWhenFocusTarget()(Code)(Java Doc) public synchronized VetoableChangeListener[] getVetoableChangeListeners()(Code)(Java Doc) public Rectangle getVisibleRect()(Code)(Java Doc) public int getWidth()(Code)(Java Doc) public int getX()(Code)(Java Doc) public int getY()(Code)(Java Doc) public void grabFocus()(Code)(Java Doc) public boolean isDoubleBuffered()(Code)(Java Doc) public static boolean isLightweightComponent(Component c)(Code)(Java Doc) public boolean isManagingFocus()(Code)(Java Doc) public boolean isOpaque()(Code)(Java Doc) public boolean isOptimizedDrawingEnabled()(Code)(Java Doc) final public boolean isPaintingForPrint()(Code)(Java Doc) public boolean isPaintingTile()(Code)(Java Doc) public boolean isRequestFocusEnabled()(Code)(Java Doc) public boolean isValidateRoot()(Code)(Java Doc) public void paint(Graphics g)(Code)(Java Doc) protected void paintBorder(Graphics g)(Code)(Java Doc) protected void paintChildren(Graphics g)(Code)(Java Doc) protected void paintComponent(Graphics g)(Code)(Java Doc) public void paintImmediately(int x, int y, int w, int h)(Code)(Java Doc) public void paintImmediately(Rectangle r)(Code)(Java Doc) protected String paramString()(Code)(Java Doc) public void print(Graphics g)(Code)(Java Doc) public void printAll(Graphics g)(Code)(Java Doc) protected void printBorder(Graphics g)(Code)(Java Doc) protected void printChildren(Graphics g)(Code)(Java Doc) protected void printComponent(Graphics g)(Code)(Java Doc) protected void processComponentKeyEvent(KeyEvent e)(Code)(Java Doc) protected boolean processKeyBinding(KeyStroke ks, KeyEvent e, int condition, boolean pressed)(Code)(Java Doc) protected void processKeyEvent(KeyEvent e)(Code)(Java Doc) protected void processMouseEvent(MouseEvent e)(Code)(Java Doc) protected void processMouseMotionEvent(MouseEvent e)(Code)(Java Doc) final public void putClientProperty(Object key, Object value)(Code)(Java Doc) public void registerKeyboardAction(ActionListener anAction, String aCommand, KeyStroke aKeyStroke, int aCondition)(Code)(Java Doc) public void registerKeyboardAction(ActionListener anAction, KeyStroke aKeyStroke, int aCondition)(Code)(Java Doc) public void removeAncestorListener(AncestorListener listener)(Code)(Java Doc) public void removeNotify()(Code)(Java Doc) public synchronized void removeVetoableChangeListener(VetoableChangeListener listener)(Code)(Java Doc) public void repaint(long tm, int x, int y, int width, int height)(Code)(Java Doc) public void repaint(Rectangle r)(Code)(Java Doc) public boolean requestDefaultFocus()(Code)(Java Doc) public void requestFocus()(Code)(Java Doc) public boolean requestFocus(boolean temporary)(Code)(Java Doc) public boolean requestFocusInWindow()(Code)(Java Doc) protected boolean requestFocusInWindow(boolean temporary)(Code)(Java Doc) public void resetKeyboardActions()(Code)(Java Doc) public void reshape(int x, int y, int w, int h)(Code)(Java Doc) public void revalidate()(Code)(Java Doc) public void scrollRectToVisible(Rectangle aRect)(Code)(Java Doc) final public void setActionMap(ActionMap am)(Code)(Java Doc) public void setAlignmentX(float alignmentX)(Code)(Java Doc) public void setAlignmentY(float alignmentY)(Code)(Java Doc) public void setAutoscrolls(boolean autoscrolls)(Code)(Java Doc) public void setBackground(Color bg)(Code)(Java Doc) public void setBorder(Border border)(Code)(Java Doc) public void setComponentPopupMenu(JPopupMenu popup)(Code)(Java Doc) public void setDebugGraphicsOptions(int debugOptions)(Code)(Java Doc) public static void setDefaultLocale(Locale l)(Code)(Java Doc) public void setDoubleBuffered(boolean aFlag)(Code)(Java Doc) public void setEnabled(boolean enabled)(Code)(Java Doc) public void setFocusTraversalKeys(int id, Set<? extends AWTKeyStroke> keystrokes)(Code)(Java Doc) public void setFont(Font font)(Code)(Java Doc) public void setForeground(Color fg)(Code)(Java Doc) public void setInheritsPopupMenu(boolean value)(Code)(Java Doc) final public void setInputMap(int condition, InputMap map)(Code)(Java Doc) public void setInputVerifier(InputVerifier inputVerifier)(Code)(Java Doc) public void setMaximumSize(Dimension maximumSize)(Code)(Java Doc) public void setMinimumSize(Dimension minimumSize)(Code)(Java Doc) public void setNextFocusableComponent(Component aComponent)(Code)(Java Doc) public void setOpaque(boolean isOpaque)(Code)(Java Doc) public void setPreferredSize(Dimension preferredSize)(Code)(Java Doc) public void setRequestFocusEnabled(boolean requestFocusEnabled)(Code)(Java Doc) public void setToolTipText(String text)(Code)(Java Doc) public void setTransferHandler(TransferHandler newHandler)(Code)(Java Doc) protected void setUI(ComponentUI newUI)(Code)(Java Doc) public void setVerifyInputWhenFocusTarget(boolean verifyInputWhenFocusTarget)(Code)(Java Doc) public void setVisible(boolean aFlag)(Code)(Java Doc) public void unregisterKeyboardAction(KeyStroke aKeyStroke)(Code)(Java Doc) public void update(Graphics g)(Code)(Java Doc) public void updateUI()(Code)(Java Doc)
|
|
|
|