public static interface KeYGuiExtension.MainMenu
JMenu
in the main frame.Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
getMainMenuActions(MainWindow mainWindow)
A list of actions which should be added to the main menu.
|
@Nonnull java.util.List<javax.swing.Action> getMainMenuActions(@Nonnull MainWindow mainWindow)
Actions should use the KeyAction.PATH
and KeyAction.PRIORITY
to control their position in the menu.
mainWindow
- the window of the main menuKeyAction
Copyright © 2003-2019 The KeY-Project.