| |
|
| java.lang.Object de.uka.ilkd.key.gui.configuration.Config
Config | public class Config (Code) | | this class is used to set some default gui properties
|
KEY_FONT_CURRENT_GOAL_VIEW | final public static String KEY_FONT_CURRENT_GOAL_VIEW(Code) | | |
KEY_FONT_GOAL_LIST_VIEW | final public static String KEY_FONT_GOAL_LIST_VIEW(Code) | | |
KEY_FONT_INNER_NODE_VIEW | final public static String KEY_FONT_INNER_NODE_VIEW(Code) | | |
KEY_FONT_PROOF_LIST_VIEW | final public static String KEY_FONT_PROOF_LIST_VIEW(Code) | | |
KEY_FONT_PROOF_TREE | final public static String KEY_FONT_PROOF_TREE(Code) | | name of different fonts
|
fireConfigChange | public synchronized void fireConfigChange()(Code) | | |
isMaximumSize | public boolean isMaximumSize()(Code) | | |
isMinimumSize | public boolean isMinimumSize()(Code) | | |
larger | public void larger()(Code) | | |
setDefaultFonts | public void setDefaultFonts()(Code) | | |
smaller | public void smaller()(Code) | | |
|
|
|