| java.lang.Object de.uka.ilkd.key.ocl.gf.GFCommand de.uka.ilkd.key.ocl.gf.LinkCommand
All known Subclasses: de.uka.ilkd.key.ocl.gf.SelfPropertiesCommand,
LinkCommand | public class LinkCommand extends GFCommand (Code) | | author: daniels author: This class represents a link to a subcategory submenu. author: When it is encountered as the executed command, the corresponding author: menu gets opened. |
Constructor Summary | |
public | LinkCommand(String subcat, PrintnameManager manager) Since LinkCommand is not a real command, that is sent to GF,
most fields are given dummy values here. |
displayText | final protected String displayText(Code) | | the text that is to be displayed in the refinement lists
|
tooltipText | final protected String tooltipText(Code) | | the text that is to be displayed as the tooltip
|
LinkCommand | public LinkCommand(String subcat, PrintnameManager manager)(Code) | | Since LinkCommand is not a real command, that is sent to GF,
most fields are given dummy values here.
The subcat is assigned its full display name and tooltip
Parameters: subcat - The subcategory of the menu behind this command Parameters: manager - The PrintnameManager, that can map subcat to itsfull name |
getDisplayText | public String getDisplayText()(Code) | | the text that is to be displayed in the refinement lists
|
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
|
|
|