public class Preferences
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
EDITOR_KEY |
static java.lang.String |
PARSER_FLAVOR_KEY |
static java.lang.String |
PARSER_RELAXED |
static java.lang.String |
PARSER_RIGID |
static java.lang.String |
SANITIZE_STACK_TRACE_KEY |
static java.lang.String |
SHOW_LAST_RESULT_KEY |
static IO.Verbosity |
verbosity |
static java.lang.String |
VERBOSITY_KEY |
Constructor and Description |
---|
Preferences() |
Modifier and Type | Method and Description |
---|---|
static void |
addChangeListener(java.util.prefs.PreferenceChangeListener listener) |
static void |
clear() |
static java.lang.String |
get(java.lang.String name) |
static java.lang.String |
get(java.lang.String name,
java.lang.String defaultValue) |
static java.lang.String |
getEditor() |
static java.lang.String |
getParserFlavor() |
static boolean |
getSanitizeStackTrace() |
static boolean |
getShowLastResult() |
static java.lang.String[] |
keys() |
static void |
put(java.lang.String name,
java.lang.String value) |
public static IO.Verbosity verbosity
public static final java.lang.String VERBOSITY_KEY
public static final java.lang.String SHOW_LAST_RESULT_KEY
public static final java.lang.String SANITIZE_STACK_TRACE_KEY
public static final java.lang.String EDITOR_KEY
public static final java.lang.String PARSER_FLAVOR_KEY
public static final java.lang.String PARSER_RIGID
public static final java.lang.String PARSER_RELAXED
public static boolean getShowLastResult()
public static boolean getSanitizeStackTrace()
public static java.lang.String getEditor()
public static java.lang.String getParserFlavor()
public static java.lang.String[] keys() throws java.util.prefs.BackingStoreException
java.util.prefs.BackingStoreException
public static java.lang.String get(java.lang.String name, java.lang.String defaultValue)
public static java.lang.String get(java.lang.String name)
public static void put(java.lang.String name, java.lang.String value)
public static void clear() throws java.util.prefs.BackingStoreException
java.util.prefs.BackingStoreException
public static void addChangeListener(java.util.prefs.PreferenceChangeListener listener)