public final class KeyStrokeManager
extends java.lang.Object
get()
methods.
The general guidelines for adding new keyboard shortcuts areModifier and Type | Field and Description |
---|---|
private static boolean |
FKEY_MACRO_SCHEME
If true, F keys are used for macros, otherwise CTRL+SHIFT+letter.
|
private static java.util.Map<java.lang.Class<?>,javax.swing.KeyStroke> |
mapping |
private static int |
MULTI_KEY_MASK
This constant holds the typical key combination to be used for auxiliary shortcuts
(
java.awt.Event#SHIFT_DOWN_MASK plus usually Event.CTRL_MASK ) |
private 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(MainWindowAction action) |
static javax.swing.KeyStroke |
get(ProofMacro macro) |
private static final boolean FKEY_MACRO_SCHEME
private static final int SHORTCUT_KEY_MASK
Event.CTRL_MASK
)private static final int MULTI_KEY_MASK
java.awt.Event#SHIFT_DOWN_MASK
plus usually Event.CTRL_MASK
)private static java.util.Map<java.lang.Class<?>,javax.swing.KeyStroke> mapping
public static javax.swing.KeyStroke get(ProofMacro macro)
public static javax.swing.KeyStroke get(MainWindowAction action)