public class OriginTermLabelsExt extends java.lang.Object implements KeYGuiExtension, KeYGuiExtension.ContextMenu, KeYGuiExtension.Tooltip, KeYGuiExtension.MainMenu, KeYGuiExtension.TermInfo
OriginTermLabel
s and OriginTermLabelVisualizer
s.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 |
---|
OriginTermLabelsExt() |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
getContextActions(KeYMediator mediator,
ContextMenuKind kind,
java.lang.Object underlyingObject)
A list of actions which should be added to the main menu.
|
java.util.List<javax.swing.Action> |
getMainMenuActions(MainWindow mainWindow)
A list of actions which should be added to the main menu.
|
java.util.List<java.lang.String> |
getTermInfoStrings(MainWindow mainWindow,
PosInSequent pos) |
java.util.List<java.lang.String> |
getTooltipStrings(MainWindow mainWindow,
PosInSequent pos) |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getTermLabelPriority
public 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
public java.util.List<javax.swing.Action> getContextActions(KeYMediator mediator, ContextMenuKind kind, java.lang.Object underlyingObject)
KeYGuiExtension.ContextMenu
Actions should use the KeyAction.PATH
and KeyAction.PRIORITY
to control their
position in the menu.
getContextActions
in interface KeYGuiExtension.ContextMenu
mediator
- the window of the main menukind
- the type of context menuunderlyingObject
- the object for which the context menu is requestedKeyAction
public java.util.List<java.lang.String> getTermInfoStrings(MainWindow mainWindow, PosInSequent pos)
getTermInfoStrings
in interface KeYGuiExtension.TermInfo
mainWindow
- the main window.pos
- the position of the term whose info shall be shown.public java.util.List<java.lang.String> getTooltipStrings(MainWindow mainWindow, PosInSequent pos)
getTooltipStrings
in interface KeYGuiExtension.Tooltip
mainWindow
- the main window.pos
- the position of the term whose info shall be shown.Copyright © 2003-2019 The KeY-Project.