From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 14 Jul 2021 22:21:38 +0000 (+0100)
Subject: script: Fix handling of mixed actions (clashing keystrokes)
X-Git-Tag: otter-0.7.2~77
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=ff054ce302f8bc803bfa59c7b57fb899ffa4ce11;p=otter.git

script: Fix handling of mixed actions (clashing keystrokes)

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---

diff --git a/templates/script.ts b/templates/script.ts
index fe80192d..48c10157 100644
--- a/templates/script.ts
+++ b/templates/script.ts
@@ -410,8 +410,12 @@ function recompute_keybindings() {
   });
   var uo_keys = Object.keys(uo_map);
   uo_keys.sort(function (ak,bk) {
-    let a = uo_map[ak]!;
-    let b = uo_map[bk]!;
+    let a = uo_map[ak];
+    let b = uo_map[bk];
+    if (a==null || b==null) return (
+      ( (!!a) as any ) -
+      ( (!!b) as any )
+    );
     return uo_kind_prec[a.kind] - uo_kind_prec[b.kind]
       || ak.localeCompare(bk);
   });
@@ -426,7 +430,8 @@ function recompute_keybindings() {
     else celem.remove();
   }
   for (var kk of uo_keys) {
-    let uo = uo_map[kk]!;
+    let uo = uo_map[kk];
+    if (!uo) continue;
     let prec = uo_kind_prec[uo.kind];
     let ent = document.createElement('div');
     ent.innerHTML = '<b>' + kk + '</b> ' + uo.desc;