public abstract class AbstractStrategyPropertyDefinition
extends java.lang.Object
StrategyProperties
.OneOfStrategyPropertyDefinition
Constructor and Description |
---|
AbstractStrategyPropertyDefinition(java.lang.String apiKey,
java.lang.String name,
java.lang.String tooltip,
AbstractStrategyPropertyDefinition... subProperties)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getApiKey()
Returns the key used in KeY's API.
|
java.lang.String |
getName()
Returns the human readable name of the property.
|
ImmutableArray<AbstractStrategyPropertyDefinition> |
getSubProperties()
Returns children which edits related properties to this.
|
java.lang.String |
getTooltip()
Returns the optional tooltip text which describes this property.
|
public AbstractStrategyPropertyDefinition(java.lang.String apiKey, java.lang.String name, java.lang.String tooltip, AbstractStrategyPropertyDefinition... subProperties)
apiKey
- The key used in KeY's API.name
- The human readable name of the property.tooltip
- The optional tooltip text which describes this property.subProperties
- Optional children which edits related properties to this.public java.lang.String getApiKey()
public java.lang.String getName()
public java.lang.String getTooltip()
public ImmutableArray<AbstractStrategyPropertyDefinition> getSubProperties()
ImmutableArray
otherwise.Copyright © 2003-2019 The KeY-Project.