public final class KeyStrokeManager
extends java.lang.Object
KeyStroke
s for proof macros and GUI actions.
If possible, all actions should ask this interface for a KeyStroke
,
by calling lookupAndOverride(Action)
.
The general guidelines for adding new keyboard shortcuts are
Modifier and Type | Field and Description |
---|---|
static boolean |
FKEY_MACRO_SCHEME
If true, F keys are used for macros, otherwise CTRL+SHIFT+letter.
|
static int |
MULTI_KEY_MASK
This constant holds the typical key combination to be used for auxiliary shortcuts
(
InputEvent.SHIFT_MASK plus usually InputEvent.CTRL_MASK ) |
static int |
SHORTCUT_KEY_MASK
This constant holds the typical key to be used for shortcuts
(usually
Event.CTRL_MASK ) |
Constructor and Description |
---|
KeyStrokeManager() |
Modifier and Type | Method and Description |
---|---|
static javax.swing.KeyStroke |
get(java.lang.Object action)
The same as
get(Object, KeyStroke) but uses the given object's class name
as key and non-default keystroke. |
static javax.swing.KeyStroke |
get(java.lang.Object action,
javax.swing.KeyStroke defaultValue)
The same as
get(Object, KeyStroke) but uses the given object's class name as key. |
static javax.swing.KeyStroke |
get(java.lang.Object action,
java.lang.String defaultValue)
The same as
get(Object, KeyStroke) but uses the given object's class name as key. |
static javax.swing.KeyStroke |
get(java.lang.String key,
javax.swing.KeyStroke defaultValue)
Get a
KeyStroke for the given key . |
static KeyStrokeSettings |
getSettings() |
static javax.swing.KeyStroke |
lookupAndOverride(javax.swing.Action action) |
static javax.swing.KeyStroke |
lookupAndOverride(javax.swing.Action action,
java.lang.String key)
Lookup a user-defined key stroke via
get(String, KeyStroke) for the given key. |
static void |
registerAction(javax.swing.Action action)
Register an action.
|
public static final int SHORTCUT_KEY_MASK
Event.CTRL_MASK
)public static final boolean FKEY_MACRO_SCHEME
public static final int MULTI_KEY_MASK
InputEvent.SHIFT_MASK
plus usually InputEvent.CTRL_MASK
)public static javax.swing.KeyStroke get(java.lang.String key, javax.swing.KeyStroke defaultValue)
KeyStroke
for the given key
.
If no KeyStroke
is defined, defaultValue
is returned.
Also thsi method sets the determined key stroke in the settings.
key
- keydefaultValue
- default valueKeyStrokeSettings
public static javax.swing.KeyStroke get(java.lang.Object action, java.lang.String defaultValue)
get(Object, KeyStroke)
but uses the given object's class name as key.action
- defaultValue
- public static javax.swing.KeyStroke get(java.lang.Object action, javax.swing.KeyStroke defaultValue)
get(Object, KeyStroke)
but uses the given object's class name as key.action
- defaultValue
- public static javax.swing.KeyStroke get(java.lang.Object action)
get(Object, KeyStroke)
but uses the given object's class name
as key and non-default keystroke.action
- public static javax.swing.KeyStroke lookupAndOverride(javax.swing.Action action)
action
- lookupAndOverride(Action, String)
public static javax.swing.KeyStroke lookupAndOverride(javax.swing.Action action, java.lang.String key)
get(String, KeyStroke)
for the given key.
If no key stroke is defined it uses the defined key stroke in the given action
.
Also adds the action to the list of actions
.
action
- key
- public static void registerAction(javax.swing.Action action)
public static KeyStrokeSettings getSettings()
Copyright © 2003-2019 The KeY-Project.