public class DecreaseFontSizeAction extends MainWindowAction implements ConfigChangeListener
Modifier and Type | Field and Description |
---|---|
private static long |
serialVersionUID
generated sUID
|
mainWindow
SHORTCUT_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
|
getMediator
getIcon, getMenuPath, getName, getPriority, getSmallIcon, getTooltip, isSelected, setAcceleratorKey, setAcceleratorLetter, setIcon, setLargeIcon, setLargeIcon, setMenuPath, setName, setPriority, setSelected, setSmallIcon, setTooltip
private 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.ActionListener
public void configChanged(ConfigChangeEvent e)
ConfigChangeListener
configChanged
in interface ConfigChangeListener