| java.lang.Object
 de.uka.ilkd.key.gui.configuration.ChoiceSettings
| ChoiceSettings | | public ChoiceSettings()(Code) | | |
| ChoiceSettings | | public ChoiceSettings(HashMap category2Default)(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)
|
| getChoices | | public HashMap getChoices()(Code) | | returns a copy of the HashMap that maps categories to
their choices.
|
| getDefaultChoices | | public HashMap getDefaultChoices()(Code) | | returns a copy of the HashMap that maps categories to
their default choices.
|
| getDefaultChoicesAsSet | | public SetOfChoice getDefaultChoicesAsSet()(Code) | | returns the current selected choices as set
|
| 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
|
| setDefaultChoices | | public void setDefaultChoices(HashMap category2Default)(Code) | | |
| updateChoices | | public void updateChoices(Namespace choiceNS, boolean remove)(Code) | | updates category2Choices if new entries are found
in choiceNS or if entries of category2Choices
are no longer present in choiceNS
Parameters:
remove - remove entries not present in choiceNS |
| writeSettings | | public void writeSettings(Properties props)(Code) | | implements the method required by the Settings interface. The
settings are written to the given Properties object. Only entries of
the form < key > = < value > (,< value >)* are allowed.
Parameters:
props - the Properties object where to write the settings as (key, value) pair |
|
|