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: //
009: //
010: package de.uka.ilkd.key.gui;
011:
012: import java.awt.BorderLayout;
013: import java.awt.GridBagConstraints;
014: import java.awt.GridBagLayout;
015: import java.awt.Insets;
016: import java.awt.event.ActionEvent;
017: import java.awt.event.ActionListener;
018: import java.util.List;
019:
020: import javax.swing.*;
021:
022: import de.uka.ilkd.key.proof.ProofAggregate;
023: import de.uka.ilkd.key.proof.init.ProblemInitializer;
024: import de.uka.ilkd.key.proof.init.ProofInputException;
025: import de.uka.ilkd.key.proof.init.ProofOblInput;
026: import de.uka.ilkd.key.proof.mgt.BasicTask;
027: import de.uka.ilkd.key.proof.mgt.Contract;
028: import de.uka.ilkd.key.proof.mgt.ContractSet;
029:
030: public class UsedMethodContractsList extends JDialog {
031:
032: private BasicTask invokedNode;
033: private KeYMediator mediator;
034: private ContractSelectionPanel mCL;
035: private Contract contract = null;
036: private static UsedMethodContractsList instance = null;
037: private ContractSet cs = null;
038: private boolean firstPO = false;
039: private boolean dispose = true;
040: private JButton jump = null;
041:
042: // Some instances are kept, some are created on the fly and
043: // garbage collected
044:
045: public static UsedMethodContractsList getInstance(
046: KeYMediator mediator, ContractSet contractSet) {
047: if (instance == null)
048: instance = new UsedMethodContractsList(null, mediator,
049: "Choose DL Contract");
050: instance.setupWindow(null, contractSet, true, false, false);
051: return instance;
052: }
053:
054: public static UsedMethodContractsList getInstance(
055: KeYMediator mediator) {
056: if (instance == null)
057: instance = new UsedMethodContractsList(null, mediator,
058: "Choose DL Contract");
059: instance.setupWindow(
060: mediator.getSelectedProof().getBasicTask(), mediator
061: .getSelectedProof().getBasicTask()
062: .getAllDLMethodContracts(), false, false, true);
063: return instance;
064: }
065:
066: private void setupWindow(BasicTask invokedNode,
067: ContractSet contractSet, boolean firstPO, boolean dispose,
068: boolean jumpEnable) {
069: this .invokedNode = invokedNode;
070: this .cs = contractSet;
071: this .firstPO = firstPO;
072: this .dispose = dispose;
073: this .mCL.setContracts(cs);
074: this .jump.setEnabled(jumpEnable);
075: }
076:
077: public UsedMethodContractsList(BasicTask invokedNode,
078: KeYMediator med) {
079: this (invokedNode, med, "Used Specifications");
080: }
081:
082: private UsedMethodContractsList(BasicTask invokedNode,
083: KeYMediator med, String title) {
084: super (new JFrame(), title);
085: if (invokedNode != null)
086: setDefaultCloseOperation(DISPOSE_ON_CLOSE);
087: else
088: setDefaultCloseOperation(HIDE_ON_CLOSE);
089: this .invokedNode = invokedNode;
090: this .mediator = med;
091: setModal(true);
092: ContractSet allMC = invokedNode != null ? invokedNode
093: .getAllMethodContracts() : null;
094: mCL = new ContractSelectionPanel(allMC, true);
095: JScrollPane scroll = new JScrollPane();
096: scroll.setViewportView(mCL);
097: scroll.setPreferredSize(new java.awt.Dimension(400, 500));
098: getContentPane().setLayout(new BorderLayout());
099: getContentPane().add(scroll, BorderLayout.CENTER);
100: JButton cancel = new JButton("Cancel");
101: cancel.addActionListener(new ActionListener() {
102: public void actionPerformed(ActionEvent e) {
103: if (dispose)
104: ((JDialog) ((JButton) e.getSource())
105: .getTopLevelAncestor()).dispose();
106: else {
107: setVisible(false);
108: }
109: }
110: });
111: jump = new JButton("Go To Proof");
112: jump.addActionListener(new ActionListener() {
113: public void actionPerformed(ActionEvent e) {
114: ((JDialog) ((JButton) e.getSource())
115: .getTopLevelAncestor()).dispose();
116: openTaskForCurrentContract();
117: }
118: });
119: JButton open = new JButton("Start New Proof");
120: open.addActionListener(new ActionListener() {
121: public void actionPerformed(ActionEvent e) {
122: if (dispose) {
123: ((JDialog) ((JButton) e.getSource())
124: .getTopLevelAncestor()).dispose();
125: Runnable proofLoader = new Runnable() {
126: public void run() {
127: openNewProofForCurrentContract();
128: }
129: };
130: KeYMediator.invokeAndWait(proofLoader);
131: } else {
132: if (firstPO) {
133: contract = mCL.getCurrentSelection();
134: setVisible(false);
135: } else {
136: setVisible(false);
137: Runnable proofLoader = new Runnable() {
138: public void run() {
139: openNewProofForCurrentContract();
140: }
141: };
142: KeYMediator.invokeAndWait(proofLoader);
143: }
144: }
145: }
146: });
147:
148: JPanel p = new JPanel(new GridBagLayout());
149: GridBagConstraints c = new GridBagConstraints();
150:
151: c.insets = new Insets(5, 20, 5, 20);
152: c.gridx = 0;
153: p.add(jump, c);
154:
155: c.gridx = 1;
156: p.add(open, c);
157:
158: c.gridx = 2;
159: p.add(cancel, c);
160: p.setAlignmentY(JPanel.BOTTOM_ALIGNMENT);
161:
162: getContentPane().add(p, BorderLayout.SOUTH);
163: getContentPane().add(new JLabel("Specifications:"),
164: BorderLayout.NORTH);
165: pack();
166: getContentPane().add(scroll);
167: }
168:
169: public void dispose() {
170: mediator.freeModalAccess(this );
171: super .dispose();
172: }
173:
174: public void setVisible(boolean show) {
175: if (show)
176: mediator.requestModalAccess(this );
177: else
178: mediator.freeModalAccess(this );
179: super .setVisible(show);
180: }
181:
182: public Contract getContract() {
183: // You can only ask once for a contract
184: Contract res = contract;
185: contract = null;
186: return res;
187: }
188:
189: private void openTaskForProof(ProofAggregate p) {
190: mediator.setProof(p.getFirstProof());
191: }
192:
193: public void openTaskForCurrentContract() {
194: Contract mC = mCL.getCurrentSelection();
195: List mCL = mC.getProofs();
196: if (mCL.size() != 0) {
197: openTaskForProof((ProofAggregate) mCL.get(0));
198: }
199: }
200:
201: public void openNewProofForCurrentContract() {
202: Contract mC = mCL.getCurrentSelection();
203: if (mC == null)
204: return;
205: ProofOblInput poin = mC.getProofOblInput(invokedNode.proof());
206: if (poin == null)
207: return;
208: ProblemInitializer pi = new ProblemInitializer(Main
209: .getInstance());
210: try {
211: pi.startProver(invokedNode.proof().env(), poin);
212: } catch (ProofInputException e) {
213: //too bad
214: }
215: }
216:
217: }
|