[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]



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).