[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:

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.