01: //Copyright (c) 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: /**
19: * The parsed format of the hmsg, that GF sents, if a command in java mode
20: * was prefixed with [something].
21: * And that something gets parsed and stored in this representation.
22: * @author daniels
23: */
24: class Hmsg {
25: /**
26: * The last read line
27: */
28: String lastline = "";
29: /**
30: * the String that should be appended to all commands of the
31: * next refinement menu
32: */
33: String appendix = null;
34: /**
35: * If the editor shall probe once again for missing subtyping witnesses.
36: * Unused.
37: */
38: boolean onceAgain = false;
39: /**
40: * If false, no commands are executed automatically
41: * in the next GF reading run
42: */
43: boolean recurse = false;
44: /**
45: * if the newObject flag should be set
46: */
47: boolean newObject = false;
48: /**
49: * if the command changed the tree, so that it has to be rebuilt
50: */
51: boolean treeChanged = false;
52: /**
53: * if the display should be cleared
54: */
55: boolean clear = false;
56:
57: /**
58: * A simple setter constructor
59: * @param lastRead The last read line
60: * @param appendix the String that should be appended to all commands of the
61: * next refinement menu
62: * @param onceAgain
63: * @param recurse If false, no commands are executed automatically
64: * in the next GF reading run
65: * @param newObject if the newObject flag should be set
66: * @param treeChanged if the command changed the tree, so that it has to be rebuilt
67: * @param clear if the display should get cleared
68: */
69: public Hmsg(String lastRead, String appendix, boolean onceAgain,
70: boolean recurse, boolean newObject, boolean treeChanged,
71: boolean clear) {
72: this.lastline = lastRead;
73: this.appendix = appendix;
74: this.onceAgain = onceAgain;
75: this.recurse = recurse;
76: this.newObject = newObject;
77: this.treeChanged = treeChanged;
78: this.clear = clear;
79: }
80: }
|