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: import java.util.logging.Level;
19:
20: /**
21: * @author daniels
22: * An object of this class represents a line in the GF abstract syntax tree
23: * in the graphical form. Well, not really, but how this line appears there
24: * and what its tooltip is is stored here.
25: * RefinedAstNodeData has its tooltip from the function it represents, not
26: * from its parent node.
27: */
28: class RefinedAstNodeData extends AstNodeData {
29:
30: protected final Printname printname;
31:
32: /**
33: * all we have to know about an already refined node is its Printname
34: * and the GF line representing it
35: * @param pname the suiting Printname, may be null if the line could
36: * not be parsed
37: * @param node the GfAstNode for the current line
38: * @param pos The position in the GF AST of this node in Haskell notation
39: * @param selected if this is the selected node in the GF AST
40: * @param constraint A constraint from a parent node, that also
41: * applies for this node.
42: */
43: public RefinedAstNodeData(Printname pname, GfAstNode node,
44: String pos, boolean selected, String constraint) {
45: super (node, pos, selected, constraint);
46: this .printname = pname;
47: if (logger.isLoggable(Level.FINEST)) {
48: logger.finest(this .toString() + " - " + position);
49: }
50: }
51:
52: /**
53: * @return the printname associated with this object
54: */
55: public Printname getPrintname() {
56: return this .printname;
57: }
58:
59: /**
60: * @return displays the tooltip of the registered Printname,
61: * which may be null
62: */
63: public String getParamTooltip() {
64: if (getPrintname() != null) {
65: return getPrintname().getTooltipText();
66: } else {
67: return null;
68: }
69: }
70:
71: }
|