2020-09-15 01:33:53 +00:00
|
|
|
const hotkeys = {};
|
2018-07-14 21:19:13 +00:00
|
|
|
|
2018-07-23 02:55:29 +00:00
|
|
|
hotkeys.HOTKEYS = {};
|
|
|
|
|
|
|
|
hotkeys.hotkey_identifier =
|
2018-07-14 21:19:13 +00:00
|
|
|
function hotkey_identifier(key, ctrlKey, shiftKey, altKey)
|
|
|
|
{
|
|
|
|
// Return the string that will represent this hotkey in the dictionary.
|
|
|
|
return key.toLowerCase() + "." + (ctrlKey & 1) + "." + (shiftKey & 1) + "." + (altKey & 1);
|
|
|
|
}
|
|
|
|
|
2018-07-23 02:55:29 +00:00
|
|
|
hotkeys.hotkey_human =
|
2018-07-14 21:19:13 +00:00
|
|
|
function hotkey_human(key, ctrlKey, shiftKey, altKey)
|
|
|
|
{
|
|
|
|
// Return the string that will be displayed to the user to represent this hotkey.
|
2020-09-03 22:02:37 +00:00
|
|
|
let mods = [];
|
2018-07-14 21:19:13 +00:00
|
|
|
if (ctrlKey) { mods.push("Ctrl"); }
|
|
|
|
if (shiftKey) { mods.push("Shift"); }
|
|
|
|
if (altKey) { mods.push("Alt"); }
|
|
|
|
mods = mods.join("+");
|
|
|
|
if (mods) { mods = mods + "+"; }
|
|
|
|
return mods + key.toUpperCase();
|
|
|
|
}
|
|
|
|
|
2018-07-23 02:55:29 +00:00
|
|
|
hotkeys.register_hotkey =
|
2020-09-03 18:47:40 +00:00
|
|
|
function register_hotkey(hotkey, action, description)
|
2018-07-14 21:19:13 +00:00
|
|
|
{
|
2020-09-03 18:47:40 +00:00
|
|
|
if (! Array.isArray(hotkey))
|
|
|
|
{
|
|
|
|
hotkey = hotkey.split(/\s+/g);
|
|
|
|
}
|
|
|
|
|
2020-09-15 01:33:53 +00:00
|
|
|
const key = hotkey.pop();
|
2020-09-03 18:47:40 +00:00
|
|
|
modifiers = hotkey.map(word => word.toLocaleLowerCase());
|
2020-09-15 01:33:53 +00:00
|
|
|
const ctrlKey = modifiers.includes("control") || modifiers.includes("ctrl");
|
|
|
|
const shiftKey = modifiers.includes("shift");
|
|
|
|
const altKey = modifiers.includes("alt");
|
2020-09-03 18:47:40 +00:00
|
|
|
|
2020-09-15 01:33:53 +00:00
|
|
|
const identifier = hotkeys.hotkey_identifier(key, ctrlKey, shiftKey, altKey);
|
|
|
|
const human = hotkeys.hotkey_human(key, ctrlKey, shiftKey, altKey);
|
2018-07-23 02:55:29 +00:00
|
|
|
hotkeys.HOTKEYS[identifier] = {"action": action, "human": human, "description": description}
|
2018-07-14 21:19:13 +00:00
|
|
|
}
|
|
|
|
|
2018-07-23 02:55:29 +00:00
|
|
|
hotkeys.should_prevent_hotkey =
|
2018-07-14 21:19:13 +00:00
|
|
|
function should_prevent_hotkey(event)
|
|
|
|
{
|
2021-10-24 01:45:52 +00:00
|
|
|
/*
|
|
|
|
If the user is currently in an input element, then the registered hotkey
|
|
|
|
will be ignored and the browser will use its default behavior.
|
|
|
|
*/
|
2018-07-14 21:19:13 +00:00
|
|
|
if (event.target.tagName == "INPUT" && event.target.type == "checkbox")
|
|
|
|
{
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2018-07-23 02:12:08 +00:00
|
|
|
return common.INPUT_TYPES.has(event.target.tagName);
|
2018-07-14 21:19:13 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-08-17 02:45:14 +00:00
|
|
|
hotkeys.show_all_hotkeys =
|
|
|
|
function show_all_hotkeys()
|
2018-07-14 21:19:13 +00:00
|
|
|
{
|
2018-08-17 02:45:14 +00:00
|
|
|
// Display an Alert with a list of all the hotkeys.
|
2020-09-03 22:02:37 +00:00
|
|
|
let lines = [];
|
2020-09-03 22:33:37 +00:00
|
|
|
for (const identifier in hotkeys.HOTKEYS)
|
2018-07-14 21:19:13 +00:00
|
|
|
{
|
2020-09-15 01:33:53 +00:00
|
|
|
const line = hotkeys.HOTKEYS[identifier]["human"] + " : " + hotkeys.HOTKEYS[identifier]["description"];
|
2018-07-14 21:19:13 +00:00
|
|
|
lines.push(line);
|
|
|
|
}
|
|
|
|
lines = lines.join("\n");
|
|
|
|
alert(lines);
|
|
|
|
}
|
|
|
|
|
2020-08-31 00:53:11 +00:00
|
|
|
hotkeys.hotkeys_listener =
|
|
|
|
function hotkeys_listener(event)
|
|
|
|
{
|
2021-10-24 01:45:52 +00:00
|
|
|
if (hotkeys.should_prevent_hotkey(event))
|
|
|
|
{
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2020-08-31 00:53:11 +00:00
|
|
|
identifier = hotkeys.hotkey_identifier(event.key, event.ctrlKey, event.shiftKey, event.altKey);
|
2021-06-04 00:53:34 +00:00
|
|
|
//console.log(identifier);
|
2020-08-31 00:53:11 +00:00
|
|
|
if (identifier in hotkeys.HOTKEYS)
|
2018-07-14 21:19:13 +00:00
|
|
|
{
|
2020-08-31 00:53:11 +00:00
|
|
|
hotkeys.HOTKEYS[identifier]["action"]();
|
|
|
|
event.preventDefault();
|
2018-07-14 21:19:13 +00:00
|
|
|
}
|
2020-08-31 00:53:11 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
window.addEventListener("keydown", hotkeys.hotkeys_listener);
|
2018-07-14 21:19:13 +00:00
|
|
|
|
2020-09-03 18:47:40 +00:00
|
|
|
hotkeys.register_hotkey("/", hotkeys.show_all_hotkeys, "Show hotkeys.");
|