run_command: actually observe "print" flag;
authorwenzelm
Sat, 03 Jul 2010 23:24:36 +0200
changeset 37688 9f047b2cfc72
parent 37687 e07dacec79e7
child 37689 628eabe2213a
run_command: actually observe "print" flag;
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 () =>