01: //Copyright (c) Kristofer Johanisson 2004, Hans-Joachim Daniels 2005
02: //
03: //This program is free software; you can redistribute it and/or modify
04: //it under the terms of the GNU General Public License as published by
05: //the Free Software Foundation; either version 2 of the License, or
06: //(at your option) any later version.
07: //
08: //This program is distributed in the hope that it will be useful,
09: //but WITHOUT ANY WARRANTY; without even the implied warranty of
10: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
11: //GNU General Public License for more details.
12: //
13: //You can either finde the file LICENSE or LICENSE.TXT in the source
14: //distribution or in the .jar file of this application
15:
16: package de.uka.ilkd.key.ocl.gf;
17:
18: import java.util.logging.Level;
19:
20: import de.uka.ilkd.key.casetool.UMLModelClass;
21:
22: /**
23: * provides a interface for letting the GF editor send class invariants back to KeY
24: * @author Kristofer Johannisson & Hans-Joachim Daniels
25: */
26: public class CallbackClassInv extends ConstraintCallback {
27: boolean useTJC;
28: Object tjc;
29: UMLModelClass rmc;
30:
31: /**
32: * send invariant to Together using methods in ReprModelClass
33: */
34: public CallbackClassInv(UMLModelClass rmc) {
35: this .rmc = rmc;
36: useTJC = false;
37: }
38:
39: /**
40: * calls the right methods to save the OCL constraints as JavaDocComments
41: * @param invOCL the OCL constraint
42: */
43: public void sendConstraint(String invOCL) {
44: if (logger.isLoggable(Level.FINE)) {
45: logger.fine("CallbackClassInv received OCL: " + invOCL);
46: }
47: final int invStart = invOCL.indexOf("inv:") + 4;
48: final String toSend = invOCL.substring(invStart);
49: if (logger.isLoggable(Level.FINE)) {
50: logger.fine("invariant: " + toSend);
51: }
52: // pass inv on to KeY
53: rmc.setMyInv(toSend);
54: rmc.setMyInvGFAbs(null); //delete that JavaDoc comment
55: }
56:
57: /**
58: * calls the right methods to save the unfinished OCL constrain
59: * as JavaDocComments in GF tree syntax
60: * @param abs the GF AST
61: */
62: public void sendAbstract(String abs) {
63: if (logger.isLoggable(Level.FINE)) {
64: logger.fine("CallbackClassInv received Abstract: " + abs);
65: }
66: // pass inv on to KeY
67: rmc.setMyInv(null); //delete that JavaDoc comment
68: rmc.setMyInvGFAbs(abs.replaceAll("\\n", " "));
69: }
70: }
|