Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
AUTO_SAVE |
private int |
autoSave
auto save is disabled by default.
|
static boolean |
disableSpecs
if true then JML specifications are globally disabled
in this run of KeY, regardless of the regular settings
|
private static java.lang.String |
DND_DIRECTION_SENSITIVE_KEY |
private boolean |
dndDirectionSensitive
is drag and drop instantiation direction sensitive
|
private java.util.LinkedList<SettingsListener> |
listenerList |
static boolean |
noPruningClosed
This parameter disables the possibility to prune in closed branches.
|
private static java.lang.String |
RIGHT_CLICK_MACROS_KEY |
private boolean |
rightClickMacros
launches the rightclick the macro menu. on by default.
|
private static java.lang.String |
TACLET_FILTER |
private boolean |
tacletFilter
minimize interaction is on by default
|
private static java.lang.String |
USE_JML_KEY |
private boolean |
useJML
JML is active by default
|
Constructor and Description |
---|
GeneralSettings() |
Modifier and Type | Method and Description |
---|---|
void |
addSettingsListener(SettingsListener l)
adds a listener to the settings object
|
int |
autoSavePeriod() |
protected void |
fireSettingsChanged()
sends the message that the state of this setting has been
changed to its registered listeners (not thread-safe)
|
boolean |
isDndDirectionSensitive() |
boolean |
isRightClickMacro() |
void |
readSettings(java.lang.Object sender,
java.util.Properties props)
gets a Properties object and has to perform the necessary
steps in order to change this object in a way that it
represents the stored settings
|
void |
removeSettingsListener(SettingsListener l)
removes the listener from the settings object
|
void |
setAutoSave(int period) |
void |
setDnDDirectionSensitivity(boolean b) |
void |
setRightClickMacros(boolean b) |
void |
setTacletFilter(boolean b) |
void |
setUseJML(boolean b) |
boolean |
tacletFilter() |
boolean |
useJML() |
void |
writeSettings(java.lang.Object sender,
java.util.Properties props)
implements the method required by the Settings interface.
|
public static boolean noPruningClosed
public static boolean disableSpecs
private static final java.lang.String TACLET_FILTER
private static final java.lang.String DND_DIRECTION_SENSITIVE_KEY
private static final java.lang.String USE_JML_KEY
private static final java.lang.String RIGHT_CLICK_MACROS_KEY
private static final java.lang.String AUTO_SAVE
private boolean tacletFilter
private boolean dndDirectionSensitive
private boolean rightClickMacros
private boolean useJML
private int autoSave
private java.util.LinkedList<SettingsListener> listenerList
public boolean tacletFilter()
public boolean isDndDirectionSensitive()
public boolean isRightClickMacro()
public boolean useJML()
public int autoSavePeriod()
public void setTacletFilter(boolean b)
public void setDnDDirectionSensitivity(boolean b)
public void setRightClickMacros(boolean b)
public void setUseJML(boolean b)
public void setAutoSave(int period)
public void readSettings(java.lang.Object sender, java.util.Properties props)
readSettings
in interface Settings
public void writeSettings(java.lang.Object sender, java.util.Properties props)
writeSettings
in interface Settings
props
- the Properties object where to write the settings as (key, value) pairprotected void fireSettingsChanged()
public void addSettingsListener(SettingsListener l)
addSettingsListener
in interface Settings
l
- the listenerpublic void removeSettingsListener(SettingsListener l)
l
- the listener to remove