# HG changeset patch
# User wenzelm
# Date 1289739908 -3600
# Node ID 9e196062bf889b2d9e4fc00ac6126534e66ae052
# Parent  e38e80686ce5582c1ba72d33c4e2bfbcf926fc19
clarified interact/print state: proof commands are treated as in TTY mode to get full response;

diff -r e38e80686ce5 -r 9e196062bf88 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Nov 13 22:33:07 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Nov 14 14:05:08 2010 +0100
@@ -197,13 +197,11 @@
   | NONE => ());
 
 fun async_state tr st =
-  if Toplevel.print_of tr orelse Keyword.is_proof (Toplevel.name_of tr) then
-    ignore
-      (Future.fork_group (Task_Queue.new_group NONE)
-        (fn () =>
-          Toplevel.setmp_thread_position tr
-            (fn () => Toplevel.print_state false st) ()))
-  else ();
+  ignore
+    (Future.fork_group (Task_Queue.new_group NONE)
+      (fn () =>
+        Toplevel.setmp_thread_position tr
+          (fn () => Toplevel.print_state false st) ()));
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -223,9 +221,12 @@
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       let
-        val int = is_some (Toplevel.init_of tr);
+        val is_init = is_some (Toplevel.init_of 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 start = start_timing ();
-        val (errs, result) = run int tr st;
+        val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
         val _ = timing tr (end_timing start);
         val _ = List.app (Toplevel.error_msg tr) errs;
         val res =
@@ -234,7 +235,7 @@
           | SOME st' =>
              (Toplevel.status tr Markup.finished;
               proof_status tr st';
-              if int then () else async_state tr st';
+              if do_print then async_state tr st' else ();
               (true, st')));
       in res end
   | Exn.Exn exn =>