de.uka.ilkd.key.gui.configuration

Class Config

java.lang.Object

de.uka.ilkd.key.gui.configuration.Config

public class Config
extends java.lang.Object

this class is used to set some default gui properties

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Config()

Method Summary

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()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

KEY_FONT_PROOF_TREE

public static final java.lang.String KEY_FONT_PROOF_TREE

name of different fonts

See Also:

Constant Field Values

KEY_FONT_SEQUENT_VIEW

public static final java.lang.String KEY_FONT_SEQUENT_VIEW

See Also:

Constant Field Values

KEY_FONT_GOAL_LIST_VIEW

public static final java.lang.String KEY_FONT_GOAL_LIST_VIEW

See Also:

Constant Field Values

KEY_FONT_PROOF_LIST_VIEW

public static final java.lang.String KEY_FONT_PROOF_LIST_VIEW

See Also:

Constant Field Values

sizes

private static final int[] sizes

An array of font sizes for the goal view

DEFAULT

public static final Config DEFAULT

sizeIndex

private int sizeIndex

The index of the current size

configChangeEvent

private ConfigChangeEvent configChangeEvent

cached ConfigChange event

listenerList

private final java.util.List<ConfigChangeListener> listenerList

the listeners to this Config

Constructor Detail

Config

private Config()

Method Detail

larger

public void larger()

smaller

public void smaller()

isMinimumSize

public boolean isMinimumSize()

isMaximumSize

public boolean isMaximumSize()

setDefaultFonts

public void setDefaultFonts()

addConfigChangeListener

public void addConfigChangeListener(ConfigChangeListener listener)

removeConfigChangeListener

public void removeConfigChangeListener(ConfigChangeListener listener)

fireConfigChange

public void fireConfigChange()