public class OneOfStrategyPropertyDefinition extends AbstractStrategyPropertyDefinition
StrategyProperties
allows the user to select predefined values.
It might be realized via radio buttons or read-only drop down boxes (combos).AbstractStrategyPropertyDefinition
,
StrategyPropertyValueDefinition
Modifier and Type | Field and Description |
---|---|
private int |
columnsPerRow
Defines optionally how many columns are shown per row.
|
private ImmutableArray<StrategyPropertyValueDefinition> |
values
The possible
StrategyPropertyValueDefinition which the user can select. |
Constructor and Description |
---|
OneOfStrategyPropertyDefinition(java.lang.String apiKey,
java.lang.String name,
AbstractStrategyPropertyDefinition[] subProperties,
StrategyPropertyValueDefinition... values)
Constructor.
|
OneOfStrategyPropertyDefinition(java.lang.String apiKey,
java.lang.String name,
int columnsPerRow,
StrategyPropertyValueDefinition... values)
Constructor.
|
OneOfStrategyPropertyDefinition(java.lang.String apiKey,
java.lang.String name,
StrategyPropertyValueDefinition... values)
Constructor.
|
OneOfStrategyPropertyDefinition(java.lang.String apiKey,
java.lang.String name,
java.lang.String tooltip,
int columnsPerRow,
AbstractStrategyPropertyDefinition[] subProperties,
StrategyPropertyValueDefinition... values)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
int |
getColumnsPerRow()
Returns the maximal columns per row.
|
ImmutableArray<StrategyPropertyValueDefinition> |
getValues()
Returns The possible
StrategyPropertyValueDefinition which the user can select. |
getApiKey, getName, getSubProperties, getTooltip
private final ImmutableArray<StrategyPropertyValueDefinition> values
StrategyPropertyValueDefinition
which the user can select.private final int columnsPerRow
public OneOfStrategyPropertyDefinition(java.lang.String apiKey, java.lang.String name, StrategyPropertyValueDefinition... values)
apiKey
- The key used in KeY's API.name
- The human readable name of the property.values
- The possible StrategyPropertyValueDefinition
which the user can select.public OneOfStrategyPropertyDefinition(java.lang.String apiKey, java.lang.String name, int columnsPerRow, StrategyPropertyValueDefinition... values)
apiKey
- The key used in KeY's API.name
- The human readable name of the property.columnsPerRow
- Defines optionally how many columns are shown per row.values
- The possible StrategyPropertyValueDefinition
which the user can select.public OneOfStrategyPropertyDefinition(java.lang.String apiKey, java.lang.String name, AbstractStrategyPropertyDefinition[] subProperties, StrategyPropertyValueDefinition... values)
apiKey
- The key used in KeY's API.name
- The human readable name of the property.subProperties
- Optional children which edits related properties to this.values
- The possible StrategyPropertyValueDefinition
which the user can select.public OneOfStrategyPropertyDefinition(java.lang.String apiKey, java.lang.String name, java.lang.String tooltip, int columnsPerRow, AbstractStrategyPropertyDefinition[] subProperties, StrategyPropertyValueDefinition... values)
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.columnsPerRow
- Defines optionally how many columns are shown per row.subProperties
- Optional children which edits related properties to this.values
- The possible StrategyPropertyValueDefinition
which the user can select.public ImmutableArray<StrategyPropertyValueDefinition> getValues()
StrategyPropertyValueDefinition
which the user can select.StrategyPropertyValueDefinition
which the user can select.public int getColumnsPerRow()