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: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17: package de.uka.ilkd.key.proof.init;
18:
19: import java.io.File;
20:
21: import javax.swing.JOptionPane;
22:
23: import de.uka.ilkd.key.gui.JMLSpecBrowser;
24: import de.uka.ilkd.key.proof.ProofAggregate;
25: import de.uka.ilkd.key.util.ProgressMonitor;
26:
27: /**
28: * This class extends the JavaInput by opening the JML Specification Browser
29: * after loading the java source files and contained JML specifications.
30: * @deprecated
31: */
32: public class JavaInputWithJMLSpecBrowser extends JavaInput {
33:
34: private JMLProofOblInput jmlPO;
35:
36: /**
37: * @param name name of the input, will be the name of the created environment
38: * @param path path of the java files
39: * @param monitor ProgressMonitor for showing progress while loading
40: */
41: public JavaInputWithJMLSpecBrowser(String name, File path,
42: boolean allIntMode, ProgressMonitor monitor) {
43: super (name, path, monitor);
44: }
45:
46: public void read(ModStrategy mod) throws ProofInputException {
47: //readProblem(mod);
48: }
49:
50: public void readProblem(ModStrategy mod) throws ProofInputException {
51: jmlPO = null;
52: int option = JOptionPane.NO_OPTION;
53: do {
54: JMLSpecBrowser sb = new JMLSpecBrowser(initConfig
55: .getServices(), readJavaPath());
56: jmlPO = sb.getPOI();
57: if (jmlPO == null) {
58: option = JOptionPane
59: .showConfirmDialog(
60: null,
61: "Do you really want to abort loading the proof?",
62: "Abort Loading",
63: JOptionPane.YES_NO_OPTION);
64: }
65: } while (option == JOptionPane.NO_OPTION && jmlPO == null);
66:
67: if (jmlPO == null) {
68: if (option == JOptionPane.YES_OPTION) {
69: throw ProofInputException.USER_ABORT_EXCEPTION;
70: }
71: throw new ProofInputException(
72: "No Proofobligation could be created.");
73: } else {
74: jmlPO.setInitConfig(getInitConfig());
75: }
76: try {
77: jmlPO.readProblem(ModStrategy.NO_GENSORTS);
78: } catch (ProofInputException e) {
79: initConfig.getServices().getExceptionHandler()
80: .reportException(e);
81: }
82: }
83:
84: /* (non-Javadoc)
85: * @see de.uka.ilkd.key.proof.init.ProofOblInput#getPO()
86: */
87: public ProofAggregate getPO() {
88: return jmlPO.getPO();
89: }
90: }
|