001: //Copyright (c) Hans-Joachim Daniels 2005
002: //
003: //This program is free software; you can redistribute it and/or modify
004: //it under the terms of the GNU General Public License as published by
005: //the Free Software Foundation; either version 2 of the License, or
006: //(at your option) any later version.
007: //
008: //This program is distributed in the hope that it will be useful,
009: //but WITHOUT ANY WARRANTY; without even the implied warranty of
010: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
011: //GNU General Public License for more details.
012: //
013: //You can either finde the file LICENSE or LICENSE.TXT in the source
014: //distribution or in the .jar file of this application
015:
016: package de.uka.ilkd.key.ocl.gf;
017:
018: import java.util.HashMap;
019: import java.util.HashSet;
020: import java.util.logging.Level;
021: import java.util.logging.Logger;
022:
023: /**
024: * @author daniels
025: * This class represents a command, that is sent to GF.
026: * TODO Refactor the chain command stuff out of this class and make it a subclass
027: */
028: class RealCommand extends GFCommand {
029:
030: /**
031: * maps shorthands to fullnames
032: */
033: private final static HashMap fullnames = new HashMap();
034:
035: private final static Logger logger = Logger
036: .getLogger(Printname.class.getName());
037:
038: /**
039: * The number of undo steps that is needed to undo this fun call
040: */
041: public final int undoSteps;
042:
043: /**
044: * The text that GF sent to describe the command
045: */
046: protected final String showText;
047:
048: protected final String subcat;
049:
050: /**
051: * Creates a Command that stands for a GF command, no link command
052: * sets all the attributes of this semi-immutable class.
053: * @param myCommand the actual GF command
054: * @param processedSubcats
055: * @param manager maps funs to previously read Printnames.
056: * Thus needs to be the same object.
057: * @param myShowText The text GF prints in the show part of the XML
058: * which should be the command followed by the printname
059: * @param mlAbstract is true, iff the menu language is set to Abstract
060: * Then no preloaded printnames are used.
061: * @param toAppend will be appended to the command, that is sent to GF.
062: * Normally, toAppend will be the empty String "".
063: * But it can be a chain command's second part.
064: * It will not be shown to the user.
065: */
066: public RealCommand(final String myCommand,
067: final HashSet processedSubcats,
068: final PrintnameManager manager, final String myShowText,
069: final boolean mlAbstract, final String toAppend) {
070: this (myCommand, processedSubcats, manager, myShowText,
071: mlAbstract, toAppend, 1, null, null);
072: }
073:
074: /**
075: * Creates a Command that stands for a GF command, no link command
076: * sets all the attributes of this semi-immutable class.
077: * @param myCommand the actual GF command
078: * @param processedSubcats
079: * @param manager maps funs to previously read Printnames.
080: * Thus needs to be the same object.
081: * @param myShowText The text GF prints in the show part of the XML
082: * which should be the command followed by the printname
083: * @param mlAbstract is true, iff the menu language is set to Abstract
084: * Then no preloaded printnames are used.
085: * @param toAppend will be appended to the command, that is sent to GF.
086: * Normally, toAppend will be the empty String "".
087: * But it can be a chain command's second part.
088: * It will not be shown to the user.
089: * @param undoSteps The number of undo steps that is needed to undo this fun call
090: * @param printnameFun If the fun, that selects the printname, should not be read from
091: * myCommand. For single commands, this is the only fun. For chain command, the last is
092: * taken. With this parameter, this behaviour can be overwritten
093: * @param subcat Normally, every fun has its own Printname, which has a fixed
094: * category. Sometimes, for the properies of self for example,
095: * this should be overwritten. If null, the subcat from the printname is used.
096: */
097: public RealCommand(final String myCommand,
098: final HashSet processedSubcats,
099: final PrintnameManager manager, final String myShowText,
100: final boolean mlAbstract, String toAppend, int undoSteps,
101: String printnameFun, String subcat) {
102: if (fullnames.isEmpty()) {
103: fullnames.put("w", "wrap");
104: fullnames.put("r", "refine");
105: fullnames.put("ch", "change head");
106: fullnames.put("rc", "refine from history:");
107: fullnames.put("ph", "peel head");
108: }
109: if (logger.isLoggable(Level.FINEST)) {
110: logger.finest("new RealCommand: " + myCommand);
111: }
112: //if we have a ChainCommand, but undoSteps is just 1, count the undoSteps.
113: if ((undoSteps == 1) && (myCommand.indexOf(";;") > -1)) {
114: int occ = Utils.countOccurances(Utils
115: .removeQuotations(myCommand), ";;") + 1;
116: this .undoSteps = occ;
117: } else {
118: this .undoSteps = undoSteps;
119: }
120: this .command = myCommand.trim();
121: this .showText = myShowText;
122: this .subcat = subcat;
123:
124: //handle chain commands.
125: //Only the last command counts for the printname selection
126: final String lastCommand;
127: if (this .undoSteps > 1) {
128: //TODO: sth. like refine " f ;;d" ;; mp [2] will break here.
129: final int chainIndex = this .command.lastIndexOf(";;");
130: lastCommand = this .command.substring(chainIndex + 2).trim();
131: } else {
132: lastCommand = this .command;
133: }
134:
135: //extract command type
136: int ind = lastCommand.indexOf(' ');
137: if (ind > -1) {
138: this .commandType = lastCommand.substring(0, ind);
139: } else {
140: this .commandType = lastCommand;
141: }
142:
143: //extract the argument position for wrapping commands and cut that part
144: if (this .commandType.equals("w")
145: || this .commandType.equals("ph")) {
146: int beforeNumber = lastCommand.lastIndexOf(' ');
147: int protoarg;
148: try {
149: String argumentAsString = lastCommand
150: .substring(beforeNumber + 1);
151: protoarg = Integer.parseInt(argumentAsString);
152: } catch (Exception e) {
153: protoarg = -1;
154: }
155: this .argument = protoarg;
156: } else {
157: this .argument = -1;
158: }
159:
160: //extract the fun of the GF command
161: if (this .commandType.equals("w")) {
162: int beforePos = lastCommand.indexOf(' ');
163: int afterPos = lastCommand.lastIndexOf(' ');
164: if (beforePos > -1 && afterPos > beforePos) {
165: this .funName = lastCommand.substring(beforePos + 1,
166: afterPos);
167: } else {
168: this .funName = null;
169: }
170: } else {
171: int beforePos = lastCommand.indexOf(' ');
172: if (beforePos > -1) {
173: this .funName = lastCommand.substring(beforePos + 1);
174: } else {
175: this .funName = null;
176: }
177: }
178:
179: //get corresponding Printname
180: if (this .commandType.equals("d")) {
181: this .printname = Printname.delete;
182: } else if (this .commandType.equals("ac")) {
183: this .printname = Printname.addclip;
184: } else if (this .commandType.equals("rc")) {
185: String subtree = this .showText.substring(3);
186: this .printname = new Printname(this .getCommand(), subtree
187: + "\\$paste the previously copied subtree here<br>"
188: + subtree, false);
189: } else if (this .commandType.equals("ph")) {
190: this .printname = Printname.peelHead(this .argument);
191: } else if (mlAbstract) {
192: //create a new Printname
193: this .printname = new Printname(funName, myShowText, null,
194: null);
195: } else { //standard case
196: if (printnameFun == null) {
197: this .printname = manager.getPrintname(funName);
198: } else {
199: //overwrite mode. Until now, only for properties of self.
200: this .printname = manager.getPrintname(printnameFun);
201: }
202: }
203:
204: if (this .getSubcat() != null) {
205: if (processedSubcats.contains(this .getSubcat())) {
206: newSubcat = false;
207: } else {
208: newSubcat = true;
209: processedSubcats.add(this .getSubcat());
210: }
211: } else {
212: newSubcat = false;
213: }
214:
215: //now append toAppend before it is too late.
216: //Only now, since it must not interfere with the things above.
217: if (toAppend != null) {
218: this .command += toAppend;
219: }
220: }
221:
222: /**
223: * the text that is to be displayed in the refinement lists
224: */
225: public String getDisplayText() {
226: String result = "";
227: if (this .printname.funPresent) {
228: result = this .printname.getDisplayText();
229: } else {
230: if (fullnames.containsKey(this .commandType)) {
231: result = fullnames.get(this .commandType) + " '";
232: }
233: result = result + this .printname.getDisplayText();
234: if (fullnames.containsKey(this .commandType)) {
235: result = result + "'";
236: }
237: }
238: if (this .commandType.equals("w")) {
239: String insertion = " as argument " + (this .argument + 1);
240: result = result + insertion;
241: }
242: if (this .printname.type != null) {
243: result = result + " : " + this .printname.type;
244: }
245: return result;
246: }
247:
248: /**
249: * the text that is to be displayed as the tooltip
250: */
251: public String getTooltipText() {
252: String result;
253: result = this .printname.getTooltipText();
254: if (this .commandType.equals("w")) {
255: String insertion = "<br>The selected sub-tree will be the "
256: + (this .argument + 1)
257: + ". argument of this refinement.";
258: result = Printname.htmlAppend(result, insertion);
259: }
260: return result;
261: }
262:
263: /**
264: * returns the subcat of this command
265: */
266: public String getSubcat() {
267: if (this .subcat == null) {
268: return this .printname.getSubcat();
269: } else {
270: //special case, only for properties of self so far
271: return this.subcat;
272: }
273: }
274: }
|