Hi all,
Ron Pressler contributed Unicode support to the TLAToolbox. Unicode support makes it possible to render TLA+ with Unicode characters. We believe Unicode support to improve readability especially for new users due to the more familiar syntax.
Unicode support works for all Toolbox windows: the TLA+ editor,
the Model Editor and the Error Trace. See the screenshot below
which show the TLA+ editor and the Error Trace with Unicode
support enabled. Unicode support works at the UI level only and
can be easily toggled via the File> "Use Unicode" menu entry.
Your .tla files do not get rewritten with Unicode characters. When
typing with Unicode support enabled, ASCII input is converted to
Unicode on-the-fly. You do not have to type Unicode.
The Unicode support required significant changes in the Toolbox code base and although the feature appears solid, we think it is best to initially release a beta version. Once we will have gathered sufficient feedback from the beta testers, we will incorporate Unicode support into the regular Toolbox release. This is why the download link at https://tla2.msr-inria.inria.fr/unicode/ wants you to enter an email address with which we might eventually solicit feedback. We will not use your email address for any other purpose.
Thanks,Markus
