# HG changeset patch
# User wenzelm
# Date 1315423910 -7200
# Node ID 3d9ee91394ce06b0210ba6468ae2946fb11163dd
# Parent  aecfefb05731a0ab5a01ede0e829c86523bedb8e
no print_state for final proof commands, which return to theory state;

diff -r aecfefb05731 -r 3d9ee91394ce src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Sep 07 21:10:47 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Sep 07 21:31:50 2011 +0200
@@ -331,7 +331,6 @@
   let
     val is_init = Toplevel.is_init tr;
     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
-    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
 
     val _ = Multithreading.interrupted ();
     val _ = Toplevel.status tr Markup.forked;
@@ -343,13 +342,18 @@
   in
     (case result of
       NONE =>
-       (if null errs then Exn.interrupt () else ();
-        Toplevel.status tr Markup.failed;
-        (st, no_print))
+        let
+          val _ = if null errs then Exn.interrupt () else ();
+          val _ = Toplevel.status tr Markup.failed;
+        in (st, no_print) end
     | SOME st' =>
-       (Toplevel.status tr Markup.finished;
-        proof_status tr st';
-        (st', if do_print then print_state tr st' else no_print)))
+        let
+          val _ = Toplevel.status tr Markup.finished;
+          val _ = proof_status tr st';
+          val do_print =
+            not is_init andalso
+              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+        in (st', if do_print then print_state tr st' else no_print) end)
   end;
 
 end;