public class Config
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ConfigChangeEvent |
configChangeEvent
cached ConfigChange event
|
static Config |
DEFAULT |
static java.lang.String |
KEY_FONT_GOAL_LIST_VIEW |
static java.lang.String |
KEY_FONT_PROOF_LIST_VIEW |
static java.lang.String |
KEY_FONT_PROOF_TREE
name of different fonts
|
static java.lang.String |
KEY_FONT_SEQUENT_VIEW |
private java.util.List<ConfigChangeListener> |
listenerList
the listeners to this Config
|
private int |
sizeIndex
The index of the current size
|
private static int[] |
sizes
An array of font sizes for the goal view
|
Modifier | Constructor and Description |
---|---|
private |
Config() |
Modifier and Type | Method and Description |
---|---|
void |
addConfigChangeListener(ConfigChangeListener listener) |
void |
fireConfigChange() |
boolean |
isMaximumSize() |
boolean |
isMinimumSize() |
void |
larger() |
void |
removeConfigChangeListener(ConfigChangeListener listener) |
void |
setDefaultFonts() |
void |
smaller() |
public static final java.lang.String KEY_FONT_PROOF_TREE
public static final java.lang.String KEY_FONT_SEQUENT_VIEW
public static final java.lang.String KEY_FONT_GOAL_LIST_VIEW
public static final java.lang.String KEY_FONT_PROOF_LIST_VIEW
private static final int[] sizes
public static final Config DEFAULT
private int sizeIndex
private ConfigChangeEvent configChangeEvent
private final java.util.List<ConfigChangeListener> listenerList
public void larger()
public void smaller()
public boolean isMinimumSize()
public boolean isMaximumSize()
public void setDefaultFonts()
public void addConfigChangeListener(ConfigChangeListener listener)
public void removeConfigChangeListener(ConfigChangeListener listener)
public void fireConfigChange()