| |
|
| java.lang.Object de.uka.ilkd.key.gui.ModelSourceSettings
ModelSourceSettings | public class ModelSourceSettings implements Settings(Code) | | |
ModelSourceSettings | public ModelSourceSettings()(Code) | | |
addSettingsListener | public void addSettingsListener(SettingsListener l)(Code) | | adds a listener to the settings object
Parameters: l - the listener |
fireSettingsChanged | protected void fireSettingsChanged()(Code) | | sends the message that the state of this setting has been
changed to its registered listeners (not thread-safe)
|
readSettings | public void readSettings(Properties props)(Code) | | 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
|
restore | public void restore()(Code) | | restores old values
|
setChanged | public void setChanged(boolean arg)(Code) | | |
setModelSource | public void setModelSource(String value)(Code) | | |
store | public void store()(Code) | | |
|
|
|