public abstract class ContextMenuAdapter extends java.lang.Object implements KeYGuiExtension.ContextMenu
Constructor and Description |
---|
ContextMenuAdapter() |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Node underlyingObject) |
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> |
getContextActions(KeYMediator mediator,
ContextMenuKind kind,
PosInSequent underlyingObject) |
java.util.List<javax.swing.Action> |
getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Proof underlyingObject) |
java.util.List<javax.swing.Action> |
getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Rule underlyingObject) |
public final 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<javax.swing.Action> getContextActions(KeYMediator mediator, ContextMenuKind kind, Proof underlyingObject)
public java.util.List<javax.swing.Action> getContextActions(KeYMediator mediator, ContextMenuKind kind, Node underlyingObject)
public java.util.List<javax.swing.Action> getContextActions(KeYMediator mediator, ContextMenuKind kind, PosInSequent underlyingObject)
public java.util.List<javax.swing.Action> getContextActions(KeYMediator mediator, ContextMenuKind kind, Rule underlyingObject)
Copyright © 2003-2019 The KeY-Project.