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: * @author daniels
20: * This class represents a link to a subcategory submenu.
21: * When it is encountered as the executed command, the corresponding
22: * menu gets opened.
23: */
24: public class LinkCommand extends GFCommand {
25:
26: /**
27: * Since LinkCommand is not a real command, that is sent to GF,
28: * most fields are given dummy values here.
29: * The subcat is assigned its full display name and tooltip
30: * @param subcat The subcategory of the menu behind this command
31: * @param manager The PrintnameManager, that can map subcat to its
32: * full name
33: */
34: public LinkCommand(final String subcat,
35: final PrintnameManager manager) {
36: this .command = subcat;
37: this .newSubcat = false;
38: this .commandType = Printname.SUBCAT;
39: this .argument = -1;
40: this .funName = null;
41: this .printname = null;
42:
43: String dtext;
44: String ttext;
45: String fullname = manager.getFullname(subcat);
46: if (fullname == null) {
47: dtext = getSubcat();
48: ttext = "open submenu " + getSubcat();
49: } else {
50: ttext = Printname.htmlPrepend(Printname
51: .extractTooltipText(fullname),
52: "<i>open submenu</i> <br> ");
53: dtext = Printname.extractDisplayText(fullname);
54: }
55: this .tooltipText = ttext;
56: this .displayText = dtext;
57:
58: }
59:
60: /**
61: * the text that is to be displayed as the tooltip
62: */
63: protected final String tooltipText;
64:
65: /**
66: * the text that is to be displayed as the tooltip
67: */
68: public String getTooltipText() {
69: return tooltipText;
70: }
71:
72: /**
73: * the text that is to be displayed in the refinement lists
74: */
75: protected final String displayText;
76:
77: /**
78: * the text that is to be displayed in the refinement lists
79: */
80: public String getDisplayText() {
81: return displayText;
82: }
83:
84: /**
85: * the subcategory of this command
86: */
87: public String getSubcat() {
88: return this.command;
89: }
90:
91: }
|