de.uka.ilkd.key.rule

Class TacletAttributes

java.lang.Object

de.uka.ilkd.key.rule.TacletAttributes

public final class TacletAttributes
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	displayName
private java.lang.String	helpText
private Trigger	trigger trigger related information

Constructor Summary

Constructors

Constructor and Description
TacletAttributes()

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

displayName

private java.lang.String displayName

helpText

private java.lang.String helpText

trigger

private Trigger trigger

trigger related information

Constructor Detail

TacletAttributes

public TacletAttributes()

Method Detail

displayName

public java.lang.String displayName()

helpText

public java.lang.String helpText()

setDisplayName

public void setDisplayName(java.lang.String s)

sets an optional display name (presented to the user)

setHelpText

public void setHelpText(java.lang.String s)

getTrigger

public Trigger getTrigger()

setTrigger

public void setTrigger(Trigger trigger)