Hi.
This issue was mentioned here over a year ago, but I think its intent got lost in the rest of the discussion, so let me bring it up again.
The TLA+ pdf pretty-printer does a fantastic job, but its output is optimized for the printed page, while I look at a screen all day and don’t even own a printer (not that I remember, at least). After months of reading and writing TLA+ almost all day, every day, the ASCII representation of various symbols is now second nature to me, but I still find it less readable than proper symbols (and people less familiar with TLA+ find it far less readable), while the pdf output sits pretty much unused.
All (or virtually all) TLA+ symbols have unicode characters. How about letting the Toolbox present the unicode representation of the escaped symbols, i.e., display ∈ when the file says \in ? Better yet, as nearly all modern text editors support unicode, how about supporting unicode as a legal, alternative representation in all tools, namely, the tla file could contain \cup, \union, or ∪ to represent union? The toolbox would then have an option of saving the symbols to the file as unicode or keeping the ASCII representation. Agda also works with unicode symbols (but I think that is the only valid representation).
Ron