run_command: actually observe "print" flag;
authorwenzelm
Sat, 03 Jul 2010 23:24:36 +0200
changeset 377049f047b2cfc72
parent 37703 e07dacec79e7
child 37705 628eabe2213a
run_command: actually observe "print" flag;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jul 03 22:33:10 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jul 03 23:24:36 2010 +0200
     1.3 @@ -561,9 +561,11 @@
     1.4  fun status tr m =
     1.5    setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
     1.6  
     1.7 -fun async_state tr st =
     1.8 -  Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
     1.9 -    setmp_thread_position tr (fn () => print_state false st) ());
    1.10 +fun async_state (tr as Transition {print, ...}) st =
    1.11 +  if print then
    1.12 +    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
    1.13 +      setmp_thread_position tr (fn () => print_state false st) ()))
    1.14 +  else ();
    1.15  
    1.16  fun error_msg tr exn_info =
    1.17    setmp_thread_position tr (fn () =>