On Tuesday, March 29, 2016 at 6:25:26 PM UTC+3, Leslie Lamport wrote:
The Toolbox's Decompose Proof command has to solve the problem of maintaining indentation while expanding definitions in a proof step.
I don't know how the toolbox communicates with TLAPS, but assuming this decomposition work is done in the toolbox, then isn't it just a matter of doing it either entirely in unicode or entirely in ASCII? Program 1 can then work on complete files only (both input and output). Or did you just mention this as an example showing that maintaining indentation can be tricky?