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)));