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, validate
public 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()