public interface KeYToolbarExtensionAdapter extends KeYGuiExtension.Toolbar
Modifier and Type | Method and Description |
---|---|
default javax.swing.JToolBar |
getToolbar(MainWindow mainWindow)
A toolbar which will be embedded into the main window.s
|
default java.util.List<javax.swing.Action> |
getToolbarActions(MainWindow mainWindow) |
default java.util.List<javax.swing.Action> getToolbarActions(MainWindow mainWindow)
mainWindow
- default javax.swing.JToolBar getToolbar(MainWindow mainWindow)
KeYGuiExtension.Toolbar
getToolbar
in interface KeYGuiExtension.Toolbar
mainWindow
- the parent of the toolbarCopyright © 2003-2019 The KeY-Project.