public final class DockingLayout extends java.lang.Object implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.MainMenu, KeYGuiExtension.Toolbar
KeYGuiExtension.ContextMenu, KeYGuiExtension.Info, KeYGuiExtension.KeyboardShortcuts, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu, KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.StatusLine, KeYGuiExtension.TermInfo, KeYGuiExtension.Toolbar, KeYGuiExtension.Tooltip
Modifier and Type | Field and Description |
---|---|
static java.io.File |
LAYOUT_FILE |
static int[] |
LAYOUT_KEYS |
static java.lang.String[] |
LAYOUT_NAMES |
static float |
SIZE_ICON_DOCK |
Constructor and Description |
---|
DockingLayout() |
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.
|
javax.swing.JToolBar |
getToolbar(MainWindow mainWindow)
A toolbar which will be embedded into the main window.s
|
void |
init(MainWindow window,
KeYMediator mediator) |
public static float SIZE_ICON_DOCK
public static final java.io.File LAYOUT_FILE
public static final java.lang.String[] LAYOUT_NAMES
public static final int[] LAYOUT_KEYS
public void init(MainWindow window, KeYMediator mediator)
init
in interface KeYGuiExtension.Startup
public javax.swing.JToolBar getToolbar(MainWindow mainWindow)
KeYGuiExtension.Toolbar
getToolbar
in interface KeYGuiExtension.Toolbar
mainWindow
- the parent of the toolbarpublic java.util.List<javax.swing.Action> getMainMenuActions(MainWindow mainWindow)
KeYGuiExtension.MainMenu
Actions should use the KeyAction.PATH
and KeyAction.PRIORITY
to control their position in the menu.
getMainMenuActions
in interface KeYGuiExtension.MainMenu
mainWindow
- the window of the main menuKeyAction
Copyright © 2003-2019 The KeY-Project.