public class UnicodeToggleAction extends MainWindowAction
Modifier and Type | Field and Description |
---|---|
static String |
NAME |
static String |
TOOL_TIP |
private SettingsListener |
viewSettingsListener
Listens for changes on
ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() . |
mainWindow, SHORTCUT_KEY_MASK
changeSupport, enabled
ACCELERATOR_KEY, ACTION_COMMAND_KEY, DEFAULT, DISPLAYED_MNEMONIC_INDEX_KEY, LARGE_ICON_KEY, LONG_DESCRIPTION, MNEMONIC_KEY, SELECTED_KEY, SHORT_DESCRIPTION, SMALL_ICON
Constructor and Description |
---|
UnicodeToggleAction(MainWindow window) |
Modifier and Type | Method and Description |
---|---|
void |
actionPerformed(ActionEvent e) |
protected void |
handleViewSettingsChanged(EventObject e) |
protected void |
updateMainWindow() |
protected void |
updateSelectedState() |
getMediator, getName, isSelected, setAcceleratorKey, setAcceleratorLetter, setIcon, setName, setSelected, setTooltip
addPropertyChangeListener, clone, firePropertyChange, getKeys, getPropertyChangeListeners, getValue, isEnabled, putValue, removePropertyChangeListener, setEnabled
public static final String NAME
public static final 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)
protected void updateSelectedState()
public void actionPerformed(ActionEvent e)
protected void updateMainWindow()
protected void handleViewSettingsChanged(EventObject e)