public static interface KeYGuiExtension.ContextMenu
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.
|
@Nonnull java.util.List<javax.swing.Action> getContextActions(@Nonnull KeYMediator mediator, @Nonnull ContextMenuKind kind, @Nonnull java.lang.Object underlyingObject)
Actions should use the KeyAction.PATH
and KeyAction.PRIORITY
to control their
position in the menu.
mediator
- the window of the main menukind
- the type of context menuunderlyingObject
- the object for which the context menu is requestedKeyAction
Copyright © 2003-2019 The KeY-Project.