I have some more thoughts on the problem of line lengths.
In this scheme, when the line runs past the edge of its pane, we simply cut it off and show an ellipsis. The user gets no opportunity to work with the terms beyond the cutoff; she simply must contract the thing with intermediate variable substitutions. There are some problems about how to implement the term rects. What are the coordinates of the term rects that aren't shown? Are they nonexistant? I suppose so.
Now here's a truly innovative idea: if a line runs past the edge of its pane, we cut off printing and put a little control arrow at the right edge of the line, indicating that there is more stuff off that edge. The user can click on the arrow to scroll the line. By scrolling an individual line, we get higher speeds and more responsiveness. My objection to this is that it's a lot of coding.
My preference is to demand clean screen layouts. If your line runs off the edge of the screen, it's your responsibility to clean it up with intermediate variables. This argues for the line cutoff idea.