public class UnicodeToggleAction extends MainWindowAction
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
NAME |
static java.lang.String |
TOOL_TIP |
private SettingsListener |
viewSettingsListener
Listens for changes on
ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() . |
mainWindow
SHORTCUT_KEY_MASK
Constructor and Description |
---|
UnicodeToggleAction(MainWindow window) |
Modifier and Type | Method and Description |
---|---|
void |
actionPerformed(java.awt.event.ActionEvent e) |
protected void |
handleViewSettingsChanged(java.util.EventObject e) |
protected void |
updateMainWindow() |
protected void |
updateSelectedState() |
getMediator
getIcon, getMenuPath, getName, getPriority, getSmallIcon, getTooltip, isSelected, setAcceleratorKey, setAcceleratorLetter, setIcon, setLargeIcon, setLargeIcon, setMenuPath, setName, setPriority, setSelected, setSmallIcon, setTooltip
public static final java.lang.String NAME
public static final java.lang.String TOOL_TIP
private final SettingsListener viewSettingsListener
ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
.
Such changes can occur in the Eclipse context when settings are changed in for instance the KeYIDE.
public UnicodeToggleAction(MainWindow window)