01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: /*
09: * Created on Apr 18, 2005
10: */
11: package de.uka.ilkd.key.gui.nodeviews;
12:
13: import java.awt.event.ActionListener;
14:
15: import javax.swing.JMenu;
16:
17: import de.uka.ilkd.key.pp.NotationInfo;
18: import de.uka.ilkd.key.rule.IteratorOfPosTacletApp;
19: import de.uka.ilkd.key.rule.ListOfPosTacletApp;
20:
21: /**
22: * This simple taclet menu displays the user a list of applicable taclets
23: * and lets select her/him one of those. It is similar to
24: * {@link de.uka.ilkd.key.gui.nodeviews.TacletMenu} but with some important differences:
25: * <ul>
26: * <li> it returns the selected taclet app and does not initiate any further
27: * action as the original {@link de.uka.ilkd.key.gui.nodeviews.TacletMenu} </li>
28: * <li> it does not display any additional menu entries like:
29: * Apply strategies here, built-in rules, abbreviation etc.
30: * </li>
31: * </ul>
32: */
33: public class SimpleTacletSelectionMenu extends JMenu {
34:
35: /**
36: * creates an instance of this menu displaying the applications stored in
37: * <tt>apps</tt>
38: * @param apps the ListOfPosTacletApp to be displayed
39: * @param info the NotationInfo used to pretty print the taclets in
40: * tooltips
41: * @param listener the ActionListener which is registered at each
42: * menu item
43: */
44: public SimpleTacletSelectionMenu(ListOfPosTacletApp apps,
45: NotationInfo info, ActionListener listener) {
46: super ("Select Rule to Apply");
47:
48: addMenuEntries(apps, info, listener);
49: }
50:
51: /**
52: * adds the given applications to the menu
53: * @param apps the ListOfPosTacletApp to be displayed
54: * @param info the NotationInfo used to pretty print the taclets in
55: * tooltips
56: * @param listener the ActionListener which is registered at each
57: * menu item
58: */
59: private void addMenuEntries(ListOfPosTacletApp apps,
60: NotationInfo info, ActionListener listener) {
61: final IteratorOfPosTacletApp it = apps.iterator();
62: while (it.hasNext()) {
63: final DefaultTacletMenuItem item = new DefaultTacletMenuItem(
64: this, it.next(), info);
65: item.addActionListener(listener);
66: add(item);
67: }
68: }
69: }
|