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.Hashtable;
019: import java.util.Vector;
020: import java.util.logging.Level;
021: import java.util.logging.Logger;
022:
023: /**
024: * @author daniels
025: *
026: * A Printname allows easy access for all the information that is crammed
027: * into a printname in the GF grammars.
028: * This information consists of (in this order!)
029: * The tooltip text which is started with \\$
030: * The subcategory which is started with \\%
031: * The longer explanation for the subcategory which directly follows the
032: * subcategory and is put into parantheses
033: * The parameter descriptions, which start with \\#name and is followed
034: * by their actual description.
035: * HTML can be used inside the descriptions and the tooltip text
036: */
037: class Printname {
038: private static Logger subcatLogger = Logger
039: .getLogger(Printname.class.getName());
040:
041: /**
042: * delete is always the same and only consists of one letter, therefore static.
043: */
044: public static final Printname delete = new Printname("d",
045: "delete current sub-tree", false);
046: /**
047: * The ac command i always the same, therefore static
048: */
049: public static final Printname addclip = new Printname(
050: "ac",
051: "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>",
052: false);
053:
054: /**
055: * @param arg The number of the argument,
056: * that will take the place of the selected fun
057: * @return a Printname for the 'ph arg' command
058: */
059: public static Printname peelHead(int arg) {
060: final String cmd = "ph " + arg;
061: final String show = "peel head " + arg
062: + "\\$removes this fun and moves its " + (arg + 1)
063: + ". argument at its place instead";
064: return new Printname(cmd, show, true);
065: }
066:
067: /**
068: * the type of the fun behind that printname (if applicable)
069: */
070: protected final String type;
071:
072: /**
073: * If the command type will already
074: * be present in the display name and does not need to be added.
075: */
076: protected final boolean funPresent;
077: /**
078: * The character that is the borderline between the text that
079: * is to be displayed in the JList and the ToolTip text
080: */
081: public final static String TT_START = "\\$";
082: /**
083: * the string that is followed by the sub-category shorthand
084: * in the refinement menu
085: */
086: public final static String SUBCAT = "\\%";
087: /**
088: * The string that is followed by a new parameter to the GF function
089: */
090: public final static String PARAM = "\\#";
091: /**
092: * If that follows "\#" in the parameter descriptions, then do an
093: * auto-coerce when this param is meta and selected
094: */
095: public final static String AUTO_COERCE = "!";
096:
097: /**
098: * the name of the fun that is used in this command
099: */
100: protected final String fun;
101:
102: /**
103: * the printname of this function
104: */
105: protected final String printname;
106:
107: /**
108: * to cache the printname, once it is constructed
109: */
110: protected String displayedPrintname = null;
111: /**
112: * the name of the module the fun belongs to
113: * null means that the function is saved without module information,
114: * "" means that a GF command is represented
115: */
116: protected final String module;
117:
118: /**
119: * the name of the module the fun belongs to
120: * null means that the function is saved without module information,
121: * "" means that a GF command is represented
122: */
123: public String getModule() {
124: return module;
125: }
126:
127: /** the qualified function name, not needed yet */
128: /*
129: public String getFunQualified() {
130: if (module != null && !module.equals("")) {
131: return module + "." + fun;
132: } else {
133: return fun;
134: }
135: }
136: */
137:
138: /**
139: * the subcategory of this command
140: */
141: protected final String subcat;
142:
143: /**
144: * the subcategory of this command
145: */
146: public String getSubcat() {
147: return subcat;
148: }
149:
150: /**
151: * The hashmap for the names of the sub categories,
152: * with the shortname starting with '%' as the key.
153: * It is important that all Printnames of one session share the same
154: * instance of Hashtable here.
155: * This field is not static because there can be several instances of
156: * the editor that shouldn't interfere.
157: */
158: protected final Hashtable subcatNameHashtable;
159:
160: /**
161: * contains the names of the paramters of this function (String).
162: * Parallel with paramTexts
163: */
164: protected final Vector paramNames = new Vector();
165:
166: /**
167: * fetches the name of the nth parameter
168: * @param n the number of the wanted paramter
169: * @return the corresponding name, null if not found
170: */
171: public String getParamName(int n) {
172: String name = null;
173: try {
174: name = (String) this .paramNames.get(n);
175: } catch (ArrayIndexOutOfBoundsException e) {
176: subcatLogger.fine(e.getLocalizedMessage());
177: }
178: return name;
179: }
180:
181: /**
182: * contains the descriptions of the paramters of this function (String).
183: * Parallel with paramNames
184: */
185: protected final Vector paramTexts = new Vector();
186:
187: /**
188: * tells, whether the nth parameter should be auto-coerced
189: * @param n the number of the parameter in question
190: * @return whether the nth parameter should be auto-coerced
191: */
192: public boolean getParamAutoCoerce(int n) {
193: boolean result = false;
194: try {
195: result = ((Boolean) this .paramAutoCoerce.get(n))
196: .booleanValue();
197: } catch (ArrayIndexOutOfBoundsException e) {
198: subcatLogger.fine(e.getLocalizedMessage());
199: }
200: return result;
201: }
202:
203: /**
204: * stores for the parameters whether they should be auto-coerced or not.
205: * parallel with paramNames
206: */
207: protected final Vector paramAutoCoerce = new Vector();
208:
209: /**
210: * Creates a Printname for a normal GF function
211: * @param myFun the function name
212: * @param myPrintname the printname given for this function
213: * @param myFullnames the Hashtable for the full names for the category
214: * names for the shortnames like \\%PREDEF
215: * @param type The type of this fun.
216: * If null, it won't be displayed in the refinement menu.
217: */
218: public Printname(String myFun, String myPrintname,
219: Hashtable myFullnames, String type) {
220: myFun = myFun.trim();
221: myPrintname = myPrintname.trim();
222: this .printname = myPrintname;
223: this .subcatNameHashtable = myFullnames;
224: this .type = type;
225: if (myFullnames == null) {
226: //if the menu language is abstract, no fullnames are loaded
227: //and the fun will be in the used showname
228: this .funPresent = true;
229: } else {
230: this .funPresent = false;
231: }
232:
233: //parse the fun name
234: {
235: int index = myFun.indexOf('.');
236: if (index > -1) {
237: //a valid fun name must not be empty
238: this .fun = myFun.substring(index + 1);
239: this .module = myFun.substring(0, index);
240: } else {
241: this .fun = myFun;
242: this .module = null;
243: }
244: }
245:
246: //parse the parameters and cut that part
247: {
248: int index = Utils.indexOfNotEscaped(myPrintname, PARAM);
249: if (index > -1) {
250: String paramPart = myPrintname.substring(index);
251: String splitString;
252: //split takes a regexp as an argument. So we have to escape the '\' again.
253: if (PARAM.startsWith("\\")) {
254: splitString = "\\" + PARAM;
255: } else {
256: splitString = PARAM;
257: }
258: String[] params = paramPart.split(splitString);
259: //don't use the first split part, since it's empty
260: for (int i = 1; i < params.length; i++) {
261: String current = params[i];
262: boolean autocoerce = false;
263: if (AUTO_COERCE.equals(current.substring(0, 1))) {
264: autocoerce = true;
265: //cut the !
266: current = current.substring(1);
267: }
268: int nameEnd = current.indexOf(' ');
269: int nameEnd2 = Utils.indexOfNotEscaped(current,
270: PARAM);
271: if (nameEnd == -1) {
272: nameEnd = current.length();
273: }
274: String name = current.substring(0, nameEnd);
275: String description;
276: if (nameEnd < current.length() - 1) {
277: description = current.substring(nameEnd + 1)
278: .trim();
279: } else {
280: description = "";
281: }
282: this .paramNames.addElement(name);
283: this .paramTexts.addElement(description);
284: this .paramAutoCoerce.addElement(new Boolean(
285: autocoerce));
286: }
287: myPrintname = myPrintname.substring(0, index);
288: }
289: }
290:
291: //extract the subcategory part and cut that part
292: {
293: int index = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
294: if (index > -1) {
295: String subcatPart = myPrintname.substring(index);
296: myPrintname = myPrintname.substring(0, index);
297: int indFull = subcatPart.indexOf('{');
298: if (indFull > -1) {
299: int indFullEnd = subcatPart.indexOf('}',
300: indFull + 1);
301: if (indFullEnd == -1) {
302: indFullEnd = subcatPart.length();
303: }
304: String fullName = subcatPart.substring(indFull + 1,
305: indFullEnd);
306: this .subcat = subcatPart.substring(0, indFull)
307: .trim();
308: this .subcatNameHashtable.put(this .subcat, fullName);
309: if (subcatLogger.isLoggable(Level.FINER)) {
310: subcatLogger.finer("new fullname '" + fullName
311: + "' for category (shortname) '"
312: + this .subcat + "'");
313: }
314: } else {
315: subcat = subcatPart.trim();
316: }
317:
318: } else {
319: this .subcat = null;
320: }
321: }
322: }
323:
324: /**
325: * a constructor for GF command that don't represent functions,
326: * like d, ph, ac
327: * @param command the GF command
328: * @param explanation an explanatory text what this command does
329: * @param funPresent If explanation already contains the fun.
330: * If true, the fun won't be printed in the refinement menu.
331: */
332: protected Printname(String command, String explanation,
333: boolean funPresent) {
334: this .fun = command;
335: this .subcatNameHashtable = null;
336: this .subcat = null;
337: this .module = "";
338: this .printname = explanation;
339: this .type = null;
340: this .funPresent = funPresent;
341: }
342:
343: /**
344: * Special constructor for bound variables.
345: * These printnames don't get saved since they don't always exist and
346: * also consist of quite few information.
347: * @param bound The name of the bound variable
348: */
349: public Printname(String bound) {
350: this .fun = bound;
351: this .subcatNameHashtable = null;
352: this .subcat = null;
353: this .module = null;
354: this .printname = bound;
355: this .type = null;
356: this .funPresent = false;
357: }
358:
359: /**
360: * the text that is to be displayed in the refinement lists
361: */
362: public String getDisplayText() {
363: String result;
364: result = extractDisplayText(this .printname);
365: return result;
366: }
367:
368: /**
369: * the text that is to be displayed as the tooltip.
370: * Will always be enclosed in <html> </html> tags.
371: */
372: public String getTooltipText() {
373: if (this .displayedPrintname != null) {
374: return this .displayedPrintname;
375: } else {
376: String result;
377: result = extractTooltipText(this .printname);
378: if (this .paramNames.size() > 0) {
379: String params = htmlifyParams();
380: //will result in <html> wrapping
381: result = htmlAppend(result, params);
382: } else {
383: //wrap in <html> by force
384: result = htmlAppend(result, "");
385: }
386: this .displayedPrintname = result;
387: return result;
388: }
389: }
390:
391: /**
392: * extracts the part of the body of the printname that is the tooltip
393: * @param myPrintname the body of the printname
394: * @return the tooltip
395: */
396: public static String extractTooltipText(String myPrintname) {
397: //if the description part of the fun has no \\$ to denote a tooltip,
398: //but the subcat description has one, than we must take extra
399: //caution
400: final int indTT = Utils
401: .indexOfNotEscaped(myPrintname, TT_START);
402: final int indSC = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
403: int ind;
404: if ((indSC > -1) && (indSC < indTT)) {
405: ind = -1;
406: } else {
407: ind = indTT;
408: }
409: String result;
410: if (ind > -1) {
411: result = myPrintname.substring(ind + TT_START.length());
412: } else {
413: result = myPrintname;
414: }
415: ind = Utils.indexOfNotEscaped(result, SUBCAT);
416: if (ind > -1) {
417: result = result.substring(0, ind);
418: }
419: ind = Utils.indexOfNotEscaped(result, PARAM);
420: if (ind > -1) {
421: result = result.substring(0, ind);
422: }
423: return result;
424: }
425:
426: /**
427: * extracts the part of the body of the printname that is the
428: * text entry for the JList
429: * @param myPrintname the body of the printname
430: * @return the one-line description of this Printname's fun
431: */
432: public static String extractDisplayText(String myPrintname) {
433: String result;
434: int ind = Utils.indexOfNotEscaped(myPrintname, TT_START);
435: if (ind > -1) {
436: result = myPrintname.substring(0, ind);
437: } else {
438: result = myPrintname;
439: }
440: ind = Utils.indexOfNotEscaped(result, SUBCAT);
441: if (ind > -1) {
442: result = result.substring(0, ind);
443: }
444: ind = Utils.indexOfNotEscaped(result, PARAM);
445: if (ind > -1) {
446: result = result.substring(0, ind);
447: }
448:
449: return result;
450: }
451:
452: /**
453: * Appends the given string insertion to original and
454: * returns the result. If original is already HTML, the appended
455: * text will get right before the </html> tag.
456: * If original is no HTML, it will be enclosed in <html>
457: * @param original The String that is to come before insertion
458: * @param insertion the String to be appended
459: * @return the aforementioned result.
460: */
461: public static String htmlAppend(String original, String insertion) {
462: StringBuffer result;
463: if (original != null) {
464: result = new StringBuffer(original);
465: } else {
466: result = new StringBuffer();
467: }
468: int htmlindex = result.indexOf("</html>");
469:
470: if (htmlindex > -1) {
471: result.insert(htmlindex, insertion);
472: } else {
473: result.insert(0, "<html>").append(insertion).append(
474: "</html>");
475: }
476: return result.toString();
477:
478: }
479:
480: /**
481: * Prepends the given string insertion to original and
482: * returns the result. If original is already HTML, the appended
483: * text will get right after the <html> tag.
484: * If original is no HTML, it will be enclosed in <html>
485: * @param original The String that is to come after insertion
486: * @param insertion the String to be appended
487: * @return the aforementioned result.
488: */
489: public static String htmlPrepend(String original, String insertion) {
490: StringBuffer result = new StringBuffer(original);
491: int htmlindex = result.indexOf("<html>");
492:
493: if (htmlindex > -1) {
494: result.insert(htmlindex, insertion);
495: } else {
496: result.insert(0, insertion).insert(0, "<html>").append(
497: "</html>");
498: }
499: return result.toString();
500:
501: }
502:
503: /**
504: * wraps a single parameter with explanatory text
505: * into <dt> and <dd> tags
506: * @param which the number of the parameter
507: * @return the resulting String, "" if the wanted parameter
508: * is not stored (illegal index)
509: */
510: protected String htmlifyParam(int which) {
511: try {
512: String result = "<dt>" + this .paramNames.get(which)
513: + "</dt>" + "<dd>" + this .paramTexts.get(which)
514: + "</dd>";
515: return result;
516: } catch (ArrayIndexOutOfBoundsException e) {
517: subcatLogger.fine(e.getLocalizedMessage());
518: return "";
519: }
520:
521: }
522:
523: /**
524: * wraps a single parameter together with its explanatory text into
525: * a HTML definition list (<dl> tags).
526: * Also the result is wrapped in <html> tags.
527: * @param which the number of the parameter
528: * @return the resulting definition list, null if the param is not found.
529: */
530: public String htmlifySingleParam(int which) {
531: String text = htmlifyParam(which);
532: if (text.equals("")) {
533: return null;
534: }
535: String result = "<html><dl>" + text + "</dl></html>";
536: return result;
537: }
538:
539: /**
540: * looks up the description for parameter number 'which' and returns it.
541: * Returns null, if no parameter description is present.
542: * @param which The number of the parameter
543: * @return s.a.
544: */
545: public String getParamDescription(int which) {
546: return (String) paramTexts.get(which);
547: }
548:
549: /**
550: * wraps all parameters together with their explanatory text into
551: * a HTML definition list (<dl> tags).
552: * No <html> tags are wrapped around here, that is sth. the caller
553: * has to do!
554: * @return the resulting definition list, "" if which is larger than
555: * the amount of stored params
556: */
557: public String htmlifyParams() {
558: if (this .paramNames.size() == 0) {
559: return "";
560: }
561: StringBuffer result = new StringBuffer(
562: "<h4>Parameters:</h4><dl>");
563: for (int i = 0; i < this .paramNames.size(); i++) {
564: result.append(htmlifyParam(i));
565: }
566: result.append("</dl>");
567: return result.toString();
568: }
569:
570: /**
571: * a testing method that is not called from KeY.
572: * Probably things like this should be automated via JUnit ...
573: * @param args not used
574: */
575: public static void main(String[] args) {
576: String SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL#alpha the first of the two and-conjoined sentences#beta the second of the and-conjoined sentences";
577: String FandS = "andS";
578: Hashtable ht = new Hashtable();
579: Printname pn = new Printname(FandS, SandS, ht, null);
580: System.out.println(pn);
581: for (int i = 0; i < pn.paramNames.size(); i++) {
582: System.out.println(pn.htmlifySingleParam(i));
583: }
584: System.out.println(pn.getTooltipText());
585: SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL";
586: FandS = "andS";
587: pn = new Printname(FandS, SandS, ht, null);
588: System.out.println("*" + pn.getTooltipText());
589: }
590:
591: public String toString() {
592: return getDisplayText() + " \n " + getTooltipText() + " ("
593: + this .paramNames.size() + ")";
594: }
595:
596: }
|