# HG changeset patch
# User wenzelm
# Date 1278192276 -7200
# Node ID 9f047b2cfc72519da87ebe7dd3162d37bb99ee21
# Parent  e07dacec79e75c062d8a5a51ae3a33ed47b6a128
run_command: actually observe "print" flag;

diff -r e07dacec79e7 -r 9f047b2cfc72 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jul 03 22:33:10 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 03 23:24:36 2010 +0200
@@ -561,9 +561,11 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
-fun async_state tr st =
-  Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
-    setmp_thread_position tr (fn () => print_state false st) ());
+fun async_state (tr as Transition {print, ...}) st =
+  if print then
+    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
+      setmp_thread_position tr (fn () => print_state false st) ()))
+  else ();
 
 fun error_msg tr exn_info =
   setmp_thread_position tr (fn () =>