001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.gui.nodeviews;
009:
010: import java.awt.BorderLayout;
011: import java.awt.Dimension;
012: import java.awt.FlowLayout;
013: import java.awt.event.ActionEvent;
014: import java.awt.event.ActionListener;
015: import java.util.Collection;
016: import java.util.Iterator;
017: import java.util.LinkedList;
018: import java.util.List;
019:
020: import javax.swing.*;
021: import javax.swing.event.ListSelectionEvent;
022: import javax.swing.event.ListSelectionListener;
023:
024: import de.uka.ilkd.key.java.Services;
025: import de.uka.ilkd.key.logic.Sequent;
026: import de.uka.ilkd.key.pp.LogicPrinter;
027: import de.uka.ilkd.key.pp.NotationInfo;
028: import de.uka.ilkd.key.pp.ProgramPrinter;
029: import de.uka.ilkd.key.rule.Taclet;
030: import de.uka.ilkd.key.rule.TacletApp;
031: import de.uka.ilkd.key.util.Debug;
032:
033: public abstract class InsertionTacletBrowserMenuItem extends JMenu
034: implements TacletMenuItem {
035:
036: /** all taclet apps the user can choose from */
037: private Collection insertionTaclets;
038: /** the added action listeners */
039: private List listenerList = new LinkedList();
040: /** the notation info to pretty print the taclet apps */
041: protected NotationInfo notInfo;
042: /** the parent frame of the selection dialog to be displayed */
043: protected JFrame parent;
044: /** the selected taclet to be applied */
045: private TacletApp selectedTaclet;
046: /** the services */
047: protected Services services;
048:
049: public InsertionTacletBrowserMenuItem(String title, JFrame parent,
050: NotationInfo notInfo, Services services) {
051:
052: super (title);
053: this .parent = parent;
054: this .notInfo = notInfo;
055: this .services = services;
056:
057: insertionTaclets = createInsertionList();
058:
059: final JMenuItem menuItem = new JMenuItem("Open Dialog");
060: menuItem.addActionListener(new ActionListener() {
061:
062: public void actionPerformed(ActionEvent e) {
063: openDialog();
064: }
065:
066: });
067:
068: menuItem.setToolTipText("Browse applicable taclets.");
069:
070: add(menuItem);
071: addSeparator();
072: }
073:
074: /**
075: * returns the list where the tacletappItems are stored
076: * (allows easy exchange for e.g. a sorted list)
077: * default: is filo
078: */
079: protected Collection createInsertionList() {
080: return new LinkedList();
081: }
082:
083: /**
084: * adds a new taclet to be displayed by this component
085: * it is assumed that the app has been tested before by
086: * {@link #isResponsible}
087: * @param app the TacletApp to be added
088: */
089: public void add(TacletApp app) {
090: insertionTaclets.add(createListItem(app));
091: final DefaultTacletMenuItem appItem = new DefaultTacletMenuItem(
092: this , app, notInfo);
093: appItem.addActionListener(new ActionListener() {
094:
095: public void actionPerformed(ActionEvent e) {
096: processTacletSelected(e);
097: }
098:
099: });
100: add(appItem);
101: }
102:
103: public void addActionListener(ActionListener listener) {
104: listenerList.add(listener);
105: }
106:
107: protected abstract Sequent checkTaclet(Taclet t);
108:
109: /** returns the selected taclet to be applied */
110: public TacletApp connectedTo() {
111: return selectedTaclet;
112: }
113:
114: public int getAppSize() {
115: return insertionTaclets.size();
116: }
117:
118: /**
119: * tests if this class is responsible for the given taclet
120: * @param t the Taclet to be checked
121: * @return true if this item implementation shall be used
122: */
123: public boolean isResponsible(Taclet t) {
124: return checkTaclet(t) != null;
125: }
126:
127: /**
128: * opens the selection dialog displaying all hidden formulas
129: * in a list and allowing the user to select the one to be added
130: */
131: public void openDialog() {
132: final JDialog dialog = new JDialog(parent, getText(), true);
133:
134: final JList selectionList = new JList(insertionTaclets
135: .toArray());
136:
137: final JScrollPane scrollPane = new JScrollPane(selectionList,
138: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
139: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
140: scrollPane.setPreferredSize(new Dimension(300, 100));
141: scrollPane.setMinimumSize(new Dimension(150, 50));
142:
143: selectionList
144: .setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
145:
146: if (getAppSize() > 0) { // should always be true
147: selectionList.setSelectedIndex(0);
148: }
149:
150: final JTextArea displayHiddenFormula = new JTextArea();
151:
152: final Object selectedValue = selectionList.getSelectedValue();
153: displayHiddenFormula
154: .setText(selectedValue == null ? ""
155: : ((TacletAppListItem) selectedValue)
156: .longDescription());
157:
158: displayHiddenFormula.setCaretPosition(0);
159:
160: displayHiddenFormula.setEditable(false);
161:
162: selectionList
163: .addListSelectionListener(new ListSelectionListener() {
164: public void valueChanged(ListSelectionEvent e) {
165: if (e.getSource() instanceof JList) {
166: final JList list = (JList) e.getSource();
167: if (list.getSelectedIndex() >= 0) {
168: if (list.getSelectedValue() instanceof TacletAppListItem) {
169: displayHiddenFormula
170: .setText(((TacletAppListItem) list
171: .getSelectedValue())
172: .longDescription());
173: }
174: } else {
175: displayHiddenFormula.setText("");
176: }
177: displayHiddenFormula.setCaretPosition(0);
178: }
179: }
180:
181: });
182:
183: final JScrollPane formulaDisplaySP = new JScrollPane(
184: displayHiddenFormula);
185:
186: final JSplitPane split = new JSplitPane(
187: JSplitPane.HORIZONTAL_SPLIT, scrollPane,
188: formulaDisplaySP) {
189: public void setUI(javax.swing.plaf.SplitPaneUI ui) {
190: try {
191: super .setUI(ui);
192: } catch (NullPointerException e) {
193: Debug
194: .out("Exception thrown by class Main at setUI");
195: }
196: }
197: }; // work around bug in
198: // com.togethersoft.util.ui.plaf.metal.OIMetalSplitPaneUI
199: selectedTaclet = null;
200:
201: final JButton cancel = new JButton("Cancel");
202: cancel.addActionListener(new ActionListener() {
203: public void actionPerformed(ActionEvent e) {
204: selectedTaclet = null;
205: dialog.setVisible(false);
206: dialog.dispose();
207: }
208: });
209:
210: final JButton apply = new JButton("Apply");
211: apply.addActionListener(new ActionListener() {
212: public void actionPerformed(ActionEvent e) {
213: final TacletAppListItem selectedItem = (TacletAppListItem) selectionList
214: .getSelectedValue();
215:
216: if (selectedItem == null) { // should never be true
217: selectedTaclet = null;
218: } else {
219: selectedTaclet = selectedItem.getTacletApp();
220: }
221:
222: dialog.setVisible(false);
223: dialog.dispose();
224: processTacletSelected(new ActionEvent(
225: InsertionTacletBrowserMenuItem.this , 0, ""));
226: }
227: });
228:
229: final JPanel buttonPanel = new JPanel();
230: buttonPanel.setLayout(new FlowLayout());
231:
232: buttonPanel.add(apply);
233: buttonPanel.add(cancel);
234:
235: dialog.getContentPane().setLayout(new BorderLayout());
236:
237: dialog.getContentPane().add(split, BorderLayout.CENTER);
238: dialog.getContentPane().add(buttonPanel, BorderLayout.SOUTH);
239:
240: dialog.setSize(500, 250);
241:
242: dialog.setVisible(true);
243:
244: }
245:
246: protected void processTacletSelected(ActionEvent e) {
247: final Iterator it = listenerList.iterator();
248: while (it.hasNext()) {
249: ((ActionListener) it.next()).actionPerformed(e);
250: }
251: }
252:
253: public void removeActionListener(ActionListener listener) {
254: listenerList.remove(listener);
255: }
256:
257: public TacletAppListItem createListItem(TacletApp app) {
258: return new TacletAppListItem(app, checkTaclet(app.taclet()),
259: notInfo, services);
260: }
261:
262: /**
263: * inner class to pretty print the formulas to be added
264: */
265: static class TacletAppListItem {
266: private final TacletApp app;
267: private final NotationInfo notInfo;
268: private final Services services;
269: private final Sequent seq;
270:
271: public TacletAppListItem(TacletApp app, Sequent seq,
272: NotationInfo notInfo, Services services) {
273: this .app = app;
274: this .seq = seq;
275: this .notInfo = notInfo;
276: this .services = services;
277: }
278:
279: public TacletApp getTacletApp() {
280: return app;
281: }
282:
283: public String shortDescription() {
284: return longDescription();
285: }
286:
287: public String longDescription() {
288: final LogicPrinter printer = new LogicPrinter(
289: new ProgramPrinter(), notInfo, services, true);
290: printer.setInstantiation(app.instantiations());
291: printer.printSequent(seq);
292: return printer.toString();
293: }
294:
295: public String toString() {
296: return longDescription();
297: }
298: }
299:
300: }
|