A proof editor window is opened onto a proof in a theorem object whenever the
ML view function is applied to the object's name in the ML top-loop.
If view is used on an theorem object with an compressed proof,
expansion of the proof is forced. This may take some time, especially
if the proof is large. Section 
describes proof
compression and expansion.