public abstract class AbstractStrategyPropertyDefinition
extends java.lang.Object
StrategyProperties
.OneOfStrategyPropertyDefinition
Modifier and Type | Field and Description |
---|---|
private java.lang.String |
apiKey
The key used in KeY's API.
|
private java.lang.String |
name
The human readable name of the property.
|
private ImmutableArray<AbstractStrategyPropertyDefinition> |
subProperties
Optional children which edits related properties to this.
|
private java.lang.String |
tooltip
The optional tooltip text which describes this property.
|
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.
|
private final java.lang.String apiKey
private final java.lang.String name
private final java.lang.String tooltip
private final ImmutableArray<AbstractStrategyPropertyDefinition> subProperties
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.