On Tuesday, March 29, 2016 at 6:45:01 PM UTC+3, Jaak Ristioja wrote:
For users of the TLA+ Toolbox only. Not everybody fits into the proposed
box.
Sure. Those not using the toolbox could either 1/ write in unicode using whatever editor they like and then feed it to the rest of the tools directly if 3 is implemented, or after running 1 if not, or, 2/ do everything in ASCII as they do today.
Nor would the Unicode conversion box fit the following
pred(S) == \A value \in S: \/ x = 1
(*NoteThisNiceCommentHere*)\/ x = 2
In the toolbox this wouldn't be a problem, as you'll edit the code in unicode and align it accordingly. In program 1, this would be a problem (I assume you've meant the disjunctions to align) which would have to be addressed.
One workaround would be to pad the replacements with spaces, e.g. "\in"
-> " ∈ ".
Note that running program 1 to convert ASCII -> Unicode is rare, and done not more than once (per file) when you decide to transition, so the padding could be cruder than what you suggest. For example, all padding could be added after the == or even at the beginning of the line. But you're right, I don't think the logic is trivial.
Ron