public class KeyboardTacletExtension extends java.lang.Object implements KeYGuiExtension, KeYGuiExtension.LeftPanel
KeYGuiExtension.ContextMenu, KeYGuiExtension.Info, KeYGuiExtension.KeyboardShortcuts, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu, KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.StatusLine, KeYGuiExtension.TermInfo, KeYGuiExtension.Toolbar, KeYGuiExtension.Tooltip
Constructor and Description |
---|
KeyboardTacletExtension() |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<TabPanel> |
getPanels(MainWindow window,
KeYMediator mediator)
Initialization and return of the sub components.
|
public java.util.Collection<TabPanel> getPanels(MainWindow window, KeYMediator mediator)
KeYGuiExtension.LeftPanel
Called before any other method; can be used to construct the UI.
getPanels
in interface KeYGuiExtension.LeftPanel
window
- parent of this extensionmediator
- the current mediatorCopyright © 2003-2019 The KeY-Project.