Re: [tlaplus] Unicode

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

Hi!

On 29.03.2016 18:06, Ron Pressler wrote:
> On Tuesday, March 29, 2016 at 5:14:56 PM UTC+3, Stephan Merz wrote:
>>
>>
>> That's a bit over-simplifying. For example, you could have
>>
>>  ...
>>  x \in { s \in S : /\ \/ A(s)
>>                       \/ B(s)
>>                    /\ C(s) }
>>
>>
>> If you replace "\in" in the first line by the corresponding Unicode 
>> symbol, you break indentation.
>>
>>
> That's not a problem because the text would be replaced *as you type*

For users of the TLA+ Toolbox only. Not everybody fits into the proposed
box. Nor would the Unicode conversion box fit the following

pred(S) == \A value \in S: \/ x == 1
(*NoteThisNiceCommentHere*)\/ x == 2

One workaround would be to pad the replacements with spaces, e.g. "\in"
-> " ∈ ".

J