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() . |
mainWindow
SHORTCUT_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() |
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 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)