Add comments for shortcuts and extract them for the manual (#2073).

1 files changed, 40 insertions, 0 deletions

diff --git a/doc/manual/shortcuts.py b/doc/manual/shortcuts.py
new file mode 100644
index 000000000..a18786799
--- /dev/null
+++ b/doc/manual/shortcuts.py
@@ -0,0 +1,40 @@
+import sys
+
+shortcuts = []
+
+for filename in sys.argv[1:]:
+    with open(filename) as f:
+        for line in f:
+            line = line.strip();
+            if line.startswith('/* [Shortcut] '):
+                desc = line[14:-2].strip()
+                parts = desc.split(':')
+                shortcuts.append(desc.split(':'))
+
+shortcuts.sort(key=lambda x: x[0])
+
+print("""
+<table id="keyboard shortcuts">
+  <title>Keyboard shortcuts</title>
+  <tgroup cols='2' align='left' colsep='1' rowsep='1'>
+    <thead>
+      <row>
+	<entry>Key</entry>
+	<entry>Action</entry>
+      </row>
+    </thead>
+    <tbody>
+""")
+
+for s in shortcuts:
+    print("      <row>")
+    print(f"        <entry>{s[0]}</entry>")
+    print(f"        <entry>{s[1]}</entry>")
+    print("      </row>")
+
+print("""
+    </tbody>
+  </tgroup>
+</table>
+""")
+