public class StrategyPropertyValueDefinition
extends java.lang.Object
OneOfStrategyPropertyDefinition
.OneOfStrategyPropertyDefinition
Modifier and Type | Field and Description |
---|---|
private java.lang.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 java.lang.String |
tooltip
The optional tooltip text which describes this value.
|
private java.lang.String |
value
The human readable value shown in the user interface control.
|
Constructor and Description |
---|
StrategyPropertyValueDefinition(java.lang.String apiValue,
java.lang.String value,
java.lang.String tooltip)
Constructor.
|
StrategyPropertyValueDefinition(java.lang.String apiValue,
java.lang.String value,
java.lang.String tooltip,
int swingGridx,
int swingWidth)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.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() |
java.lang.String |
getTooltip()
Returns The optional tooltip text which describes this value.
|
java.lang.String |
getValue()
Returns The human readable value shown in the user interface control.
|
private final java.lang.String apiValue
private final java.lang.String value
private final java.lang.String tooltip
private final int swingGridx
private final int swingWidth
public StrategyPropertyValueDefinition(java.lang.String apiValue, java.lang.String value, java.lang.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(java.lang.String apiValue, java.lang.String value, java.lang.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 java.lang.String getApiValue()
public java.lang.String getValue()
public java.lang.String getTooltip()
public int getSwingGridx()
public int getSwingWidth()