Proposal: allow Unicode alternatives for module delimiters

[ahelwer]

Instead of:

---- MODULE Demo ----
EXTENDS Foo, Bar
---------------------
Spec == TRUE
=====================

We can allow Unicode/DOS box-drawing characters to have it resemble the generated LaTeX modules:

┌─── MODULE Demo ───┐
EXTENDS Foo, Bar
─────────────────────
Spec ≜ TRUE
└───────────────────┘

This translation is easily performed by TLAUC, and for as-you-type translation if somebody types ---- it can be replaced with ┌──┐ and if they type ==== it can be replaced by └──┘. The user can then copy/paste these characters to get a line of the desired length, and remove the end caps if they only want an internal delimiter.