public class Config
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
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 |
static int[] |
SIZES
An array of font sizes for the goal view
|
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
public static final int[] SIZES
public static final Config DEFAULT
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()
Copyright © 2003-2019 The KeY-Project.