[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Unicode TLA+
I'd like to get peoples' thoughts on this. Currently, the TLA+ tools only accept ASCII TLA+. ASCII TLA+ is also what I spend my time looking at while I'm writing TLA+ specs. However, it would be neat to have the ASCII symbols translated into their Unicode math equivalents in real time as I am typing, similar to Mathematica (if you've ever used that). I hope to get a demo of this up and running for my talk
at the TLA+ conference at the end of September. To that end, I've added support for unicode symbols to the TLA+ tree-sitter parser
and am writing a simple utility
to translate TLA+ files from ASCII to Unicode and back as a prelude to getting the real-time translator working (probably as a Neovim treesitter
module). I should mention Unicode TLA+ is an old idea, dating back at least five years to Ron Pressler's work
trying to get SANY to support Unicode, and maybe as early as Specifying Systems
where Leslie speculates that some non-ASCII TLA+ version might come along in the future. I've fleshed out a TLA+ Unicode proposal (with discussion of design decisions and drawbacks) in this document
, and you can see the list of proposed symbol translations (nicely formatted by github!) in the .csv in that directory.
Some questions to provoke discussion:
- Do you believe you would personally find it useful/easier to see TLA+ specs in their Unicode form as you are writing them?
- If you are a non-English user, would you find it useful to be able to use non-ASCII characters in identifiers (operator/module/function names, etc.) or strings?
- Do you agree with the Unicode symbol choices or have any suggestions?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/80539612-bc6e-4d23-95ff-dc7e1c6af50fn%40googlegroups.com.