From d1b315a2cb2e46abbb4ec1bba296c716ef77e268 Mon Sep 17 00:00:00 2001
From: Michiel Borkent <michielborkent@gmail.com>
Date: Tue, 21 Nov 2023 17:25:25 +0100
Subject: [PATCH] better keys

---
 public/squint/js/demo.mjs | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/public/squint/js/demo.mjs b/public/squint/js/demo.mjs
index 3bae077..81c6d8f 100644
--- a/public/squint/js/demo.mjs
+++ b/public/squint/js/demo.mjs
@@ -117,3 +117,32 @@ let editorElt = document.querySelector('#editor');
 let editor = new EditorView({state: state,
                              parent: editorElt,
                              extensions: extensions })
+
+let keys = {"ArrowUp": "↑",
+            "ArrowDown": "↓",
+            "ArrowRight": "→",
+            "ArrowLeft": "←",
+            "Mod": "Ctrl"}
+
+let macKeys = {"Alt": "⌥",
+                "Shift": "⇧",
+                "Enter": "⏎",
+                "Ctrl": "⌃",
+               "Mod": "⌘"}
+
+let mac;
+
+if (/^(Mac)|(iPhone)|(iPad)|(iPod)$/.test(window.navigator.platform.substring(0,3))) {
+  mac = true;
+  Object.assign(keys, macKeys);
+}
+
+document.querySelectorAll(".mod,.alt,.ctrl").forEach(node => {
+  let k = node.innerHTML;
+  let symbol = keys[k];
+  if (symbol) {
+    node.innerHTML = symbol;
+  }
+}
+
+)