Package | Description |
---|---|
de.uka.ilkd.key.gui.extension.api | |
de.uka.ilkd.key.gui.extension.impl | |
de.uka.ilkd.key.gui.originlabels | |
org.key_project.exploration |
Modifier and Type | Class and Description |
---|---|
class |
DefaultContextMenuKind |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Node underlyingObject) |
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
java.lang.Object underlyingObject) |
java.util.List<javax.swing.Action> |
KeYGuiExtension.ContextMenu.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> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
PosInSequent underlyingObject) |
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Proof underlyingObject) |
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Rule underlyingObject) |
Modifier and Type | Method and Description |
---|---|
static void |
KeYGuiExtensionFacade.addContextMenuItems(ContextMenuKind kind,
javax.swing.JPopupMenu menu,
java.lang.Object underlyingObject,
KeYMediator mediator) |
static javax.swing.JPopupMenu |
KeYGuiExtensionFacade.createContextMenu(ContextMenuKind kind,
java.lang.Object underlyingObject,
KeYMediator mediator) |
static javax.swing.JMenu |
KeYGuiExtensionFacade.createTermMenu(ContextMenuKind kind,
java.lang.Object underlyingObject,
KeYMediator mediator) |
java.util.List<javax.swing.Action> |
TestExtension.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
java.lang.Object underlyingObject) |
static java.util.List<javax.swing.Action> |
KeYGuiExtensionFacade.getContextMenuItems(ContextMenuKind kind,
java.lang.Object underlyingObject,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
OriginTermLabelsExt.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
java.lang.Object underlyingObject) |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
ExplorationExtension.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
java.lang.Object underlyingObject) |
Copyright © 2003-2019 The KeY-Project.