public class DecreaseFontSizeAction extends MainWindowAction implements ConfigChangeListener
| Modifier and Type | Field and Description |
|---|---|
private static long |
serialVersionUID
generated sUID
|
mainWindowSHORTCUT_KEY_MASK| Constructor and Description |
|---|
DecreaseFontSizeAction(MainWindow mainWindow)
creates the action to decrease the font size of the sequent and proof view
|
| Modifier and Type | Method and Description |
|---|---|
void |
actionPerformed(java.awt.event.ActionEvent e) |
void |
configChanged(ConfigChangeEvent e)
focused node has changed
|
getMediatorgetIcon, getMenuPath, getName, getPriority, getSmallIcon, getTooltip, isSelected, setAcceleratorKey, setAcceleratorLetter, setIcon, setLargeIcon, setLargeIcon, setMenuPath, setName, setPriority, setSelected, setSmallIcon, setTooltipprivate static final long serialVersionUID
public DecreaseFontSizeAction(MainWindow mainWindow)
mainWindow - the main windowpublic void actionPerformed(java.awt.event.ActionEvent e)
actionPerformed in interface java.awt.event.ActionListenerpublic void configChanged(ConfigChangeEvent e)
ConfigChangeListenerconfigChanged in interface ConfigChangeListener