src/Pure/PIDE/command.ML
changeset 53696 ddaf277e0d8c
parent 53673 3a35ce87a55c
child 53703 52a0eacf04d1
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 08 12:00:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 08 12:07:06 2013 +0200
     1.3 @@ -252,10 +252,13 @@
     1.4  
     1.5  (* overall execution process *)
     1.6  
     1.7 +fun run_print ({name, pri, print_process, ...}: print) =
     1.8 +  (if Multithreading.enabled () then
     1.9 +    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
    1.10 +  else memo_eval) print_process;
    1.11 +
    1.12  fun execute (({eval_process, ...}, prints): exec) =
    1.13 - (memo_eval eval_process;
    1.14 -  prints |> List.app (fn {name, pri, print_process, ...} =>
    1.15 -    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
    1.16 +  (memo_eval eval_process; List.app run_print prints);
    1.17  
    1.18  fun stable_goals exec_id =
    1.19    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));