Constructor and Description |
---|
TermLabelSettings() |
Modifier and Type | Method and Description |
---|---|
void |
addSettingsListener(SettingsListener l)
adds a listener to the settings object
|
protected void |
fireSettingsChanged()
Notify all listeners of the current state of this settings object.
|
boolean |
getUseOriginLabels() |
void |
readSettings(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 a listener from this settings object.
|
void |
setUseOriginLabels(boolean useOriginLabels)
Sets the value returned by
getUseOriginLabels() |
void |
writeSettings(java.util.Properties props)
The settings to store are written to the given Properties object.
|
public void readSettings(java.util.Properties props)
Settings
readSettings
in interface Settings
public void writeSettings(java.util.Properties props)
Settings
writeSettings
in interface Settings
props
- the Properties object where to write the settings as (key, value) pairpublic boolean getUseOriginLabels()
true
iff OriginTermLabel
s should be used.public void setUseOriginLabels(boolean useOriginLabels)
getUseOriginLabels()
useOriginLabels
- whether OriginTermLabel
s should be used.public void addSettingsListener(SettingsListener l)
Settings
addSettingsListener
in interface Settings
l
- the listenerpublic void removeSettingsListener(SettingsListener l)
removeSettingsListener
in interface Settings
l
- the listener to remove.protected void fireSettingsChanged()
Copyright © 2003-2019 The KeY-Project.