So I propose we split this into three subproblems, and I think this can work for everybody:
1. Write a program that can convert an ASCII tla file to a unicode one and vice-versa. This is where most of the logic is (indentation...), and the code can be based on the pretty printer's code.
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).
3. Modify SANY so that it can parse unicode directly. Once this is done, program 1 would be used only for conversions from each representation for upgrade/support reasons.
I volunteer to work on 1 (I can start in a few weeks), and then maybe 3 when we get there. I think 2 should be done by someone with good familiarity with Eclipse.
Ron