public class GeneralPreferencesElement extends PreferencesElement
| Constructor and Description |
|---|
GeneralPreferencesElement(SettingsElement parent)
Creates a new instance of the element for a general preferences under the settings
element.
|
| Modifier and Type | Method and Description |
|---|---|
VariableElement |
createVariable()
Adds a definition of a new variable element.
|
void |
setName(java.lang.String value)
Sets the name of the file with preferences.
|
getName, getVariables, getVersion, setVersion, validatepublic GeneralPreferencesElement(SettingsElement parent)
parent - The parent settings element of this preferences one.public void setName(java.lang.String value)
value - A name of the file with preferences.public VariableElement createVariable()