public class StrategyPropertyValueDefinition extends Object
OneOfStrategyPropertyDefinition
.OneOfStrategyPropertyDefinition
Modifier and Type | Field and Description |
---|---|
private String |
apiValue
The value used by KeY's API.
|
private int |
swingGridx
The optional hint for Swing user interfaces how to place the control used to edit the represented settings value.
|
private int |
swingWidth |
private String |
tooltip
The optional tooltip text which describes this value.
|
private String |
value
The human readable value shown in the user interface control.
|
Constructor and Description |
---|
StrategyPropertyValueDefinition(String apiValue,
String value,
String tooltip)
Constructor.
|
StrategyPropertyValueDefinition(String apiValue,
String value,
String tooltip,
int swingGridx,
int swingWidth)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
String |
getApiValue()
Returns The value used by KeY's API.
|
int |
getSwingGridx()
Returns the optional hint for Swing user interfaces how to place the control used to edit the represented settings value.
|
int |
getSwingWidth() |
String |
getTooltip()
Returns The optional tooltip text which describes this value.
|
String |
getValue()
Returns The human readable value shown in the user interface control.
|
private final String apiValue
private final String value
private final String tooltip
private final int swingGridx
private final int swingWidth
public StrategyPropertyValueDefinition(String apiValue, String value, String tooltip)
apiValue
- The value used by KeY's API.value
- The human readable value shown in the user interface control.tooltip
- The optional tooltip text which describes this value.public StrategyPropertyValueDefinition(String apiValue, String value, String tooltip, int swingGridx, int swingWidth)
apiValue
- The value used by KeY's API.value
- The human readable value shown in the user interface control.tooltip
- The optional tooltip text which describes this value.swingGridx
- The optional hint for Swing user interfaces how to place the control used to edit the represented settings value or a negative number if not defined.public String getApiValue()
public String getValue()
public String getTooltip()
public int getSwingGridx()
public int getSwingWidth()