Below is a picture of Isabelle Proof General 3.0 running inside XEmacs.
We are replaying a proof in Isar, Isabelle's new proof language developed by Markus Wenzel.

The top half of the window displays the proof script.

The blue highlighted region is the part of the script which has been sent to the proof process so far. It cannot be edited.

The bottom half of the window displays the output from Isabelle at each stage of the proof.