| javax.swing.JMenu de.uka.ilkd.key.gui.nodeviews.SimpleTacletSelectionMenu
SimpleTacletSelectionMenu | public class SimpleTacletSelectionMenu extends JMenu (Code) | | This simple taclet menu displays the user a list of applicable taclets
and lets select her/him one of those. It is similar to
de.uka.ilkd.key.gui.nodeviews.TacletMenu but with some important differences:
- it returns the selected taclet app and does not initiate any further
action as the original
de.uka.ilkd.key.gui.nodeviews.TacletMenu
- it does not display any additional menu entries like:
Apply strategies here, built-in rules, abbreviation etc.
|
SimpleTacletSelectionMenu | public SimpleTacletSelectionMenu(ListOfPosTacletApp apps, NotationInfo info, ActionListener listener)(Code) | | creates an instance of this menu displaying the applications stored in
apps
Parameters: apps - the ListOfPosTacletApp to be displayed Parameters: info - the NotationInfo used to pretty print the taclets in tooltips Parameters: listener - the ActionListener which is registered at each menu item |
Fields inherited from javax.swing.JMenu | protected WinListener popupListener(Code)(Java Doc)
|
|
|