public final class GoalBackAction extends MainWindowAction
mainWindow
CHECKBOX, LOCAL_ACCELERATOR, PATH, PRIORITY, SHORTCUT_FOCUSED_CONDITION, SHORTCUT_KEY_MASK
Constructor and Description |
---|
GoalBackAction(MainWindow mainWindow,
boolean longName)
Creates a new GoalBackAction.
|
Modifier and Type | Method and Description |
---|---|
void |
actionPerformed(java.awt.event.ActionEvent e) |
void |
initListeners()
Registers the action at some listeners to update its status
in a correct fashion.
|
void |
updateName()
Adds the displayName of the rule, which is affected by the undo operation, to the action.
|
getMediator, setAcceleratorKey, setAcceleratorLetter
getAcceleratorKey, getIcon, getMenuPath, getMnemonic, getName, getPriority, getSmallIcon, getTooltip, isSelected, lookupAcceleratorKey, lookupAcceleratorKey, setIcon, setLargeIcon, setLargeIcon, setMenuPath, setMnemonic, setName, setPriority, setSelected, setSmallIcon, setTooltip
public GoalBackAction(MainWindow mainWindow, boolean longName)
mainWindow
- the main window this action belongs tolongName
- true iff long names (including the name of the rule to undo)
shall be displayed (e.g. in menu items)public void initListeners()
public void updateName()
public void actionPerformed(java.awt.event.ActionEvent e)
Copyright © 2003-2019 The KeY-Project.