More work on Ref doc, & stuff.

implementations/as_dl.py

@@ -0,0 +1,21 @@
+from html import escape
+from re import sub
+
+
+def j_replace(match):
+    name = escape(match.group(0))
+    return f'<a href="#{name}">{name}</a>'
+
+def j_bod(body):
+    return sub('[^ [\]]+', j_replace, body.strip())
+
+defs = list(open('defs.txt'))
+
+print('<dl>')
+
+for d in defs:
+    name, body = d.split(None, 1)
+    name = escape(name)
+    print(f'	<dt id="{name}">{name}</dt> <dd>{j_bod(body)}</dd><br>')
+
+print('</dl>')