implementations/as_dl.py

   1 from html import escape
   2 from re import sub
   3
   4
   5 def j_replace(match):
   6     name = escape(match.group(0))
   7     return f'<a href="#{name}">{name}</a>'
   8
   9 def j_bod(body):
  10     return sub('[^ [\]]+', j_replace, body.strip())
  11
  12 defs = list(open('defs.txt'))
  13
  14 print('<dl>')
  15
  16 for d in defs:
  17     name, body = d.split(None, 1)
  18     name = escape(name)
  19     print(f'    <dt id="{name}">{name}</dt> <dd>{j_bod(body)}</dd><br>')
  20
  21 print('</dl>')