public static interface KeYGuiExtension.KeyboardShortcuts
KeyStrokeManager
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
GOAL_LIST |
static java.lang.String |
INFO_VIEW |
static java.lang.String |
MAIN_WINDOW |
static java.lang.String |
PROOF_TREE_VIEW |
static java.lang.String |
SEQUENT_VIEW |
static java.lang.String |
SOURCE_VIEW |
static java.lang.String |
STRATEGY_SELECTION_VIEW |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<javax.swing.Action> |
getShortcuts(KeYMediator mediator,
java.lang.String componentId,
javax.swing.JComponent component) |
static final java.lang.String SEQUENT_VIEW
static final java.lang.String GOAL_LIST
static final java.lang.String PROOF_TREE_VIEW
static final java.lang.String MAIN_WINDOW
static final java.lang.String INFO_VIEW
static final java.lang.String STRATEGY_SELECTION_VIEW
static final java.lang.String SOURCE_VIEW
java.util.Collection<javax.swing.Action> getShortcuts(KeYMediator mediator, java.lang.String componentId, javax.swing.JComponent component)
mediator
- component
- Copyright © 2003-2019 The KeY-Project.