| java.lang.Object
 de.uka.ilkd.key.ocl.gf.Printname
| Printname | | class Printname (Code) | |
author:
daniels
author:
A Printname allows easy access for all the information that is crammed
author:
into a printname in the GF grammars.
author:
This information consists of (in this order!)
author:
The tooltip text which is started with \\$
author:
The subcategory which is started with \\%
author:
The longer explanation for the subcategory which directly follows the
author:
subcategory and is put into parantheses
author:
The parameter descriptions, which start with \\#name and is followed
author:
by their actual description.
author:
HTML can be used inside the descriptions and the tooltip text |
| Constructor Summary | |
| public | Printname(String myFun, String myPrintname, Hashtable myFullnames, String type)
Creates a Printname for a normal GF function
Parameters:
myFun - the function name
Parameters:
myPrintname - the printname given for this function
Parameters:
myFullnames - the Hashtable for the full names for the categorynames for the shortnames like \\%PREDEF
Parameters:
type - The type of this fun. | | protected | Printname(String command, String explanation, boolean funPresent)
| | public | Printname(String bound)
Special constructor for bound variables. |
| AUTO_COERCE | | final public static String AUTO_COERCE(Code) | | If that follows "\#" in the parameter descriptions, then do an
auto-coerce when this param is meta and selected
|
| PARAM | | final public static String PARAM(Code) | | The string that is followed by a new parameter to the GF function
|
| SUBCAT | | final public static String SUBCAT(Code) | | the string that is followed by the sub-category shorthand
in the refinement menu
|
| TT_START | | final public static String TT_START(Code) | | The character that is the borderline between the text that
is to be displayed in the JList and the ToolTip text
|
| addclip | | final public static Printname addclip(Code) | | The ac command i always the same, therefore static
|
| delete | | final public static Printname delete(Code) | | delete is always the same and only consists of one letter, therefore static.
|
| displayedPrintname | | protected String displayedPrintname(Code) | | to cache the printname, once it is constructed
|
| fun | | final protected String fun(Code) | | the name of the fun that is used in this command
|
| funPresent | | final protected boolean funPresent(Code) | | If the command type will already
be present in the display name and does not need to be added.
|
| module | | final protected String module(Code) | | the name of the module the fun belongs to
null means that the function is saved without module information,
"" means that a GF command is represented
|
| paramAutoCoerce | | final protected Vector paramAutoCoerce(Code) | | stores for the parameters whether they should be auto-coerced or not.
parallel with paramNames
|
| paramNames | | final protected Vector paramNames(Code) | | contains the names of the paramters of this function (String).
Parallel with paramTexts
|
| paramTexts | | final protected Vector paramTexts(Code) | | contains the descriptions of the paramters of this function (String).
Parallel with paramNames
|
| printname | | final protected String printname(Code) | | the printname of this function
|
| subcat | | final protected String subcat(Code) | | the subcategory of this command
|
| subcatNameHashtable | | final protected Hashtable subcatNameHashtable(Code) | | The hashmap for the names of the sub categories,
with the shortname starting with '%' as the key.
It is important that all Printnames of one session share the same
instance of Hashtable here.
This field is not static because there can be several instances of
the editor that shouldn't interfere.
|
| type | | final protected String type(Code) | | the type of the fun behind that printname (if applicable)
|
| Printname | | public Printname(String myFun, String myPrintname, Hashtable myFullnames, String type)(Code) | | Creates a Printname for a normal GF function
Parameters:
myFun - the function name
Parameters:
myPrintname - the printname given for this function
Parameters:
myFullnames - the Hashtable for the full names for the categorynames for the shortnames like \\%PREDEF
Parameters:
type - The type of this fun. If null, it won't be displayed in the refinement menu. |
| Printname | | protected Printname(String command, String explanation, boolean funPresent)(Code) | | a constructor for GF command that don't represent functions,
like d, ph, ac
Parameters:
command - the GF command
Parameters:
explanation - an explanatory text what this command does
Parameters:
funPresent - If explanation already contains the fun.If true, the fun won't be printed in the refinement menu. |
| Printname | | public Printname(String bound)(Code) | | Special constructor for bound variables.
These printnames don't get saved since they don't always exist and
also consist of quite few information.
Parameters:
bound - The name of the bound variable |
| extractDisplayText | | public static String extractDisplayText(String myPrintname)(Code) | | extracts the part of the body of the printname that is the
text entry for the JList
Parameters:
myPrintname - the body of the printname the one-line description of this Printname's fun |
| extractTooltipText | | public static String extractTooltipText(String myPrintname)(Code) | | extracts the part of the body of the printname that is the tooltip
Parameters:
myPrintname - the body of the printname the tooltip |
| getDisplayText | | public String getDisplayText()(Code) | | the text that is to be displayed in the refinement lists
|
| getModule | | public String getModule()(Code) | | the name of the module the fun belongs to
null means that the function is saved without module information,
"" means that a GF command is represented
|
| getParamAutoCoerce | | public boolean getParamAutoCoerce(int n)(Code) | | tells, whether the nth parameter should be auto-coerced
Parameters:
n - the number of the parameter in question whether the nth parameter should be auto-coerced |
| getParamDescription | | public String getParamDescription(int which)(Code) | | looks up the description for parameter number 'which' and returns it.
Returns null, if no parameter description is present.
Parameters:
which - The number of the parameter s.a. |
| getParamName | | public String getParamName(int n)(Code) | | fetches the name of the nth parameter
Parameters:
n - the number of the wanted paramter the corresponding name, null if not found |
| getSubcat | | public String getSubcat()(Code) | | the subcategory of this command
|
| getTooltipText | | public String getTooltipText()(Code) | | the text that is to be displayed as the tooltip.
Will always be enclosed in <html> </html> tags.
|
| htmlAppend | | public static String htmlAppend(String original, String insertion)(Code) | | Appends the given string insertion to original and
returns the result. If original is already HTML, the appended
text will get right before the </html> tag.
If original is no HTML, it will be enclosed in <html>
Parameters:
original - The String that is to come before insertion
Parameters:
insertion - the String to be appended the aforementioned result. |
| htmlPrepend | | public static String htmlPrepend(String original, String insertion)(Code) | | Prepends the given string insertion to original and
returns the result. If original is already HTML, the appended
text will get right after the <html> tag.
If original is no HTML, it will be enclosed in <html>
Parameters:
original - The String that is to come after insertion
Parameters:
insertion - the String to be appended the aforementioned result. |
| htmlifyParam | | protected String htmlifyParam(int which)(Code) | | wraps a single parameter with explanatory text
into <dt> and <dd> tags
Parameters:
which - the number of the parameter the resulting String, "" if the wanted parameteris not stored (illegal index) |
| htmlifyParams | | public String htmlifyParams()(Code) | | wraps all parameters together with their explanatory text into
a HTML definition list (<dl> tags).
No <html> tags are wrapped around here, that is sth. the caller
has to do!
the resulting definition list, "" if which is larger thanthe amount of stored params |
| htmlifySingleParam | | public String htmlifySingleParam(int which)(Code) | | wraps a single parameter together with its explanatory text into
a HTML definition list (<dl> tags).
Also the result is wrapped in <html> tags.
Parameters:
which - the number of the parameter the resulting definition list, null if the param is not found. |
| main | | public static void main(String[] args)(Code) | | a testing method that is not called from KeY.
Probably things like this should be automated via JUnit ...
Parameters:
args - not used |
| peelHead | | public static Printname peelHead(int arg)(Code) | |
Parameters:
arg - The number of the argument, that will take the place of the selected fun a Printname for the 'ph arg' command |
|
|