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: /**
019: * @author daniels
020: * A class that represents a GF command together with its printname.
021: * It also gives easy access to all the abuses of the printname like
022: * the subcategory, the tooltip, it knows about wrapping and so on.
023: *
024: * The static stuff could produce problems if the editor is started
025: * several times without closing it first. It probably should be moved
026: * into a manager class.
027: * Or the instances that get generated during one run all share the same
028: * "pseudo-static" Hashtables. This is probably better.
029: *
030: */
031: abstract class GFCommand implements Comparable {
032:
033: /**
034: * the subcategory of this command
035: */
036: public abstract String getSubcat();
037:
038: /**
039: * the type of the command, r,w,ch,d,ac,...
040: */
041: protected String commandType;
042:
043: /**
044: * the type of the command, r,w,ch,d,ac,...
045: */
046: public String getCommandType() {
047: return commandType;
048: }
049:
050: /**
051: * for wrap, the number of the argument the current node should become
052: */
053: protected int argument;
054:
055: /**
056: * the actual command that this object should represent
057: */
058: protected String command;
059:
060: /**
061: * the actual command that this object should represent
062: */
063: public String getCommand() {
064: return command;
065: }
066:
067: /**
068: * the Printname corresponding to the GF fun of this command
069: */
070: protected Printname printname;
071:
072: /**
073: * the Printname corresponding to the GF fun of this command
074: */
075: public Printname getPrintname() {
076: return printname;
077: }
078:
079: /**
080: * the text that is to be displayed as the tooltip
081: */
082: public abstract String getTooltipText();
083:
084: /**
085: * the text that is to be displayed in the refinement lists
086: */
087: public abstract String getDisplayText();
088:
089: /**
090: * the name of the fun that is used in this command
091: */
092: protected String funName;
093:
094: /**
095: * if this is the first occurence of the current subcat
096: */
097: protected boolean newSubcat;
098:
099: /**
100: * if this is the first occurence of the current subcat
101: */
102: public boolean isNewSubcat() {
103: return newSubcat;
104: }
105:
106: /**
107: * Compares two GFCommands.
108: * LinkCommands are the least. Then the InputCommand (more than one
109: * does not happen). If that does not decide, the display name as a String does.
110: * @param o the other command.
111: * @return see above.
112: */
113: public int compareTo(Object o) {
114: if (this .equals(o)) {
115: return 0;
116: }
117: if (this instanceof LinkCommand && !(o instanceof LinkCommand)) {
118: return -1;
119: }
120: if (!(this instanceof LinkCommand)
121: && (o instanceof LinkCommand)) {
122: return 1;
123: }
124: //LinkCommands are dealt with, so from now on, they don't occur
125: if (this instanceof InputCommand
126: && !(o instanceof InputCommand)) {
127: return -1;
128: }
129: if (!(this instanceof InputCommand)
130: && (o instanceof InputCommand)) {
131: return 1;
132: }
133: if (!(o instanceof GFCommand)) {
134: //This should never occur!
135: return -1;
136: } else {
137: GFCommand ocmd = (GFCommand) o;
138: return this .getDisplayText().compareTo(
139: ocmd.getDisplayText());
140: }
141: }
142:
143: public String toString() {
144: return getDisplayText() + " \n " + getTooltipText();
145: }
146:
147: }
|