That looks good. The next problem is whether javacc 4.0, the version of JavaCC that produces the lexing code for SANY, works with Unicode. (The odds of SANY's JavaCC input working with a newer version seem slim.) The documentation I have for it says that it does handle Unicode characters, but the code it produces contains a lot of chars, so that claim needs to be tested. If it does, then it shouldn't be too hard to modify SANY--assuming that the relevant code works with strings rather than chars. TLC shouldn't need any changes. Modifications to the Toolbox shouldn't be too difficult, if the appropriate fonts can be used and the Eclipse code can deal with them. The interface for typing the non-ASCII characters needs to be designed. And we'd need to decide if non-ASCII characters and things like Greek letters should be allowed in identifiers. I don't know about TLAPS; but it shouldn't be a problem since I imagine OCaml handles Unicode gracefully and the new version of TLAPS will use the SANY parser. Modifications to the pretty-printer should be straightforward.
It sounds like about two person-months of work. As I wrote, I'd be happy to help guide a volunteer. But, before any work is done on it, we should find out how many people would use it. I expect that Unicode would introduce problems sharing specs that don't exist with ASCII. I personally will not trust any non-ASCII files to be usable 20 years from now.
Leslie
On Monday, March 28, 2016 at 9:10:26 AM UTC-7, Ron Pressler wrote:
DejaVu Mono is a fixed-width TTF font that seems like it has all the necessary glyphs (see page 26 of
this document), it is free, and while the Toolbox uses SWT and I don't know how that toolkit renders fonts, I see no reason why it shouldn't be possible.
Ron
On Monday, March 28, 2016 at 6:45:44 PM UTC+3, Leslie Lamport wrote:
Hi Ron,
There is one potential problem that would make a Unicode version of TLA+ impossible: because of TLA+'s use of indentation, it would require a fixed-width Unicode font. So I suggest that you investigate whether one exists and can be used by ordinary Java programs. If it does, then this would not be too hard to implement, and I would be happy to help a volunteer do it.
Leslie