de.uka.ilkd.key.strategy.definition

Class StrategyPropertyValueDefinition

java.lang.Object

de.uka.ilkd.key.strategy.definition.StrategyPropertyValueDefinition

public class StrategyPropertyValueDefinition
extends java.lang.Object

Defines a single value a user can select in the user interface control defined by a OneOfStrategyPropertyDefinition.

Author:

Martin Hentschel

See Also:

OneOfStrategyPropertyDefinition

Field Summary

Fields

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 Summary

Constructors

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.

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

apiValue

private final java.lang.String apiValue

The value used by KeY's API.

value

private final java.lang.String value

The human readable value shown in the user interface control.

tooltip

private final java.lang.String tooltip

The optional tooltip text which describes this value.

swingGridx

private final int swingGridx

The optional hint for Swing user interfaces how to place the control used to edit the represented settings value. A negative number means that it is not defined.

swingWidth

private final int swingWidth

Constructor Detail

StrategyPropertyValueDefinition

public StrategyPropertyValueDefinition(java.lang.String apiValue,
                                       java.lang.String value,
                                       java.lang.String tooltip)

Constructor.

Parameters:

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.

StrategyPropertyValueDefinition

public StrategyPropertyValueDefinition(java.lang.String apiValue,
                                       java.lang.String value,
                                       java.lang.String tooltip,
                                       int swingGridx,
                                       int swingWidth)

Constructor.

Parameters:

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.

Method Detail

getApiValue

public java.lang.String getApiValue()

Returns The value used by KeY's API.

Returns:

The value used by KeY's API.

getValue

public java.lang.String getValue()

Returns The human readable value shown in the user interface control.

Returns:

The human readable value shown in the user interface control.

getTooltip

public java.lang.String getTooltip()

Returns The optional tooltip text which describes this value.

Returns:

The optional tooltip text which describes this value.

getSwingGridx

public int getSwingGridx()

Returns the optional hint for Swing user interfaces how to place the control used to edit the represented settings value.

Returns:

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.

getSwingWidth

public int getSwingWidth()