Constructor and Description |
---|
NewSMTTranslationSettings() |
NewSMTTranslationSettings(NewSMTTranslationSettings toCopy) |
Modifier and Type | Method and Description |
---|---|
void |
addSettingsListener(SettingsListener l)
adds a listener to the settings object
|
NewSMTTranslationSettings |
clone() |
void |
copy(NewSMTTranslationSettings newTranslationSettings) |
java.lang.String |
get(java.lang.String key) |
java.util.Map<java.lang.String,java.lang.String> |
getMap() |
java.lang.String |
put(java.lang.String key,
java.lang.String value) |
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 to the settings object
|
void |
writeSettings(java.util.Properties props)
The settings to store are written to the given Properties object.
|
public NewSMTTranslationSettings()
public NewSMTTranslationSettings(NewSMTTranslationSettings toCopy)
public NewSMTTranslationSettings clone()
clone
in class java.lang.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 java.util.Map<java.lang.String,java.lang.String> getMap()
public java.lang.String get(java.lang.String key)
public java.lang.String put(java.lang.String key, java.lang.String value)
public void addSettingsListener(SettingsListener l)
Settings
addSettingsListener
in interface Settings
l
- the listenerpublic void removeSettingsListener(SettingsListener l)
Settings
removeSettingsListener
in interface Settings
l
- the listenerpublic void copy(NewSMTTranslationSettings newTranslationSettings)
Copyright © 2003-2019 The KeY-Project.