[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Unicode

2. Add an option in the toolbox so that it replaces, say, \in to ∈ as I type. Then, it uses program 1 to run SANY/TLC. I see no reason why this should be a read-only mode, and there is no complex indentation logic here (the file produced is unicode with correct indentation, and then program 1 converts it to ASCII with correct indentation).

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.