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.
Stephan |