public interface KeYMainMenuExtension
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
getMainMenuActions(MainWindow mainWindow) |
default int |
getPriority() |
java.util.List<javax.swing.Action> getMainMenuActions(MainWindow mainWindow)
mainWindow
- default int getPriority()