public final class HidePackagePrefixToggleAction extends MainWindowAction
| Modifier and Type | Field and Description |
|---|---|
static java.lang.String |
NAME |
private static long |
serialVersionUID |
static java.lang.String |
TOOL_TIP |
private SettingsListener |
viewSettingsListener
Listens for changes on
ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(). |
mainWindowSHORTCUT_KEY_MASK| Constructor and Description |
|---|
HidePackagePrefixToggleAction(MainWindow mainWindow) |
| 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() |
getMediatorgetIcon, getMenuPath, getName, getPriority, getSmallIcon, getTooltip, isSelected, setAcceleratorKey, setAcceleratorLetter, setIcon, setLargeIcon, setLargeIcon, setMenuPath, setName, setPriority, setSelected, setSmallIcon, setTooltippublic static final java.lang.String NAME
public static final java.lang.String TOOL_TIP
private static final long serialVersionUID
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 HidePackagePrefixToggleAction(MainWindow mainWindow)