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: //
10:
11: /* Generated by Together */
12:
13: package de.uka.ilkd.key.casetool.together.scripts.menuextension;
14:
15: import java.io.File;
16:
17: import javax.swing.JFileChooser;
18: import javax.swing.JFrame;
19:
20: import com.togethersoft.openapi.ide.project.IdeProjectManagerAccess;
21:
22: import de.uka.ilkd.key.casetool.FunctionalityOnModel;
23: import de.uka.ilkd.key.casetool.UMLModelClass;
24:
25: public class ClassMenuPoint4 extends ClassMenu {
26:
27: static File lastDirectory = null;
28:
29: private File directory;
30:
31: public String getMenuEntry() {
32: return "DL Proof Obligation";
33: }
34:
35: protected String runCore(UMLModelClass modelClass) {
36:
37: if (lastDirectory == null) {
38: String tprFile = IdeProjectManagerAccess
39: .getProjectManager().getActiveProject()
40: .getFileName();
41: String projectRoot = tprFile.substring(0, tprFile
42: .lastIndexOf(File.separator));
43: directory = new File(projectRoot);
44: } else {
45: directory = lastDirectory;
46: }
47: JFileChooser jFC = new JFileChooser(directory);
48: File sugg = new File(jFC.getCurrentDirectory() + File.separator
49: + "DL_PO.key");
50: if (sugg.exists()) {
51: jFC.setSelectedFile(sugg);
52: }
53: jFC.setDialogTitle("Load a .key file with the current model");
54: int load = jFC.showOpenDialog(new JFrame());
55: if (load == JFileChooser.APPROVE_OPTION) {
56: File file = jFC.getSelectedFile();
57: return FunctionalityOnModel
58: .proveDLFormula(modelClass, file);
59: }
60: return "";
61: }
62: }
|