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: package de.uka.ilkd.key.gui;
09:
10: import java.awt.event.ActionEvent;
11: import java.awt.event.ActionListener;
12: import java.util.Iterator;
13: import java.util.LinkedList;
14: import java.util.List;
15:
16: import javax.swing.JFrame;
17: import javax.swing.JMenuItem;
18:
19: import de.uka.ilkd.key.gui.nodeviews.BuiltInRuleMenuItem;
20: import de.uka.ilkd.key.logic.Constraint;
21: import de.uka.ilkd.key.logic.PosInOccurrence;
22: import de.uka.ilkd.key.proof.Proof;
23: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
24: import de.uka.ilkd.key.rule.BuiltInRule;
25: import de.uka.ilkd.key.rule.ContractConfigurator;
26: import de.uka.ilkd.key.rule.MethodContractRuleApp;
27: import de.uka.ilkd.key.rule.UseMethodContractRule;
28:
29: public class UseMethodContractRuleItem extends JMenuItem implements
30: BuiltInRuleMenuItem {
31:
32: private UseMethodContractRule connectedTo;
33: private Proof proof;
34: private PosInOccurrence pos;
35: private MethodContractRuleApp app;
36: private JFrame parent;
37:
38: /** the added action listeners */
39: private List listenerList = new LinkedList();
40:
41: public UseMethodContractRuleItem(JFrame parent,
42: UseMethodContractRule rule, Proof proof, PosInOccurrence pos) {
43: super (rule.name().toString());
44: this .connectedTo = rule;
45: this .pos = pos;
46: this .parent = parent;
47: this .proof = proof;
48:
49: super .addActionListener(new ActionListener() {
50:
51: public void actionPerformed(ActionEvent e) {
52: openDialog(e);
53: }
54:
55: });
56:
57: }
58:
59: public void openDialog(ActionEvent e) {
60: ContractConfigurator config = new DefaultContractConfigurator(
61: "Contract Configurator", parent);
62: OldOperationContract mc = connectedTo.selectContract(proof,
63: pos, config);
64: if (mc != null) {
65: app = new MethodContractRuleApp(connectedTo, pos,
66: Constraint.BOTTOM, mc);
67: processUseMethodContractRuleSelected(e);
68: }
69: }
70:
71: public BuiltInRule connectedTo() {
72: return connectedTo;
73: }
74:
75: public MethodContractRuleApp getRuleApp() {
76: return app;
77: }
78:
79: protected void processUseMethodContractRuleSelected(ActionEvent e) {
80: final Iterator it = listenerList.iterator();
81: while (it.hasNext()) {
82: ((ActionListener) it.next()).actionPerformed(e);
83: }
84: }
85:
86: public void addActionListener(ActionListener listener) {
87: listenerList.add(listener);
88: }
89:
90: public void removeActionListener(ActionListener listener) {
91: listenerList.remove(listener);
92: }
93:
94: }
|