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: /** @author Kristofer Johannisson */package de.uka.ilkd.key.casetool.together.scripts.menuextension;
10:
11: import javax.swing.ProgressMonitor;
12:
13: import org.apache.log4j.Logger;
14:
15: import de.uka.ilkd.key.casetool.ModelMethod;
16: import de.uka.ilkd.key.casetool.together.TogetherGFInterface;
17: import de.uka.ilkd.key.casetool.together.TogetherModelMethod;
18: import de.uka.ilkd.key.ocl.gf.CallbackPrePost;
19: import de.uka.ilkd.key.ocl.gf.Utils;
20:
21: public class OpMenuPoint2 extends OpMenu {
22: protected static Logger timelogger = Logger
23: .getLogger("de.uka.ilkd.key.ocl.gf.Timer");
24: protected static Logger logger = Logger.getLogger("key.ocl.gf");
25:
26: public String getMenuEntry() {
27: return "Edit Pre/Postcondition [GF]";
28: }
29:
30: public String getSubMenuName() {
31: return null;
32: }
33:
34: protected String runCore(ModelMethod modelMethod) {
35: if (timelogger.isDebugEnabled()) {
36: timelogger.debug(System.currentTimeMillis()
37: + " ObMenuPoint6 runCore");
38: }
39: if (logger.isDebugEnabled()) {
40: logger.debug("Class: "
41: + modelMethod.getContainingClassName());
42: logger
43: .debug("Signature: "
44: + modelMethod.getCallSignature());
45: }
46: pm = new ProgressMonitor(null, "Loading the GF editor for OCL",
47: "", 0, 9700);
48: Utils.tickProgress(pm, 1, "Initializing TogetherGFInterface");
49:
50: TogetherGFInterface tgfi = new TogetherGFInterface();
51: TogetherModelMethod trpmm;
52: try {
53: trpmm = (TogetherModelMethod) modelMethod;
54: } catch (ClassCastException e) {
55: String s = "This shouldn't happen: " + e;
56: System.err.println(s);
57: e.printStackTrace();
58: return s;
59: }
60: String abs = modelMethod.getMyGFAbs();
61: return (tgfi.editPrePost(trpmm.getContainingClassName(), trpmm
62: .getContainingPackage(), trpmm
63: .getCallSignatureQualified(), trpmm.getMyPreCond(),
64: trpmm.getMyPostCond(),
65: new CallbackPrePost(modelMethod), trpmm.isQuery(), pm,
66: abs)); //TODO this may return not the same as UMLOCLBehaviouralFeature.isQuery
67: }
68: }
|