public final class TacletAttributes
extends java.lang.Object
Constructor and Description |
---|
TacletAttributes() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
displayName() |
Trigger |
getTrigger() |
java.lang.String |
helpText() |
void |
setDisplayName(java.lang.String s)
sets an optional display name (presented to the user)
|
void |
setHelpText(java.lang.String s) |
void |
setTrigger(Trigger trigger) |
public java.lang.String displayName()
public java.lang.String helpText()
public void setDisplayName(java.lang.String s)
public void setHelpText(java.lang.String s)
public Trigger getTrigger()
public void setTrigger(Trigger trigger)
Copyright © 2003-2019 The KeY-Project.