src/Pure/PIDE/command.ML
changeset 52559 ddaf277e0d8c
parent 52536 3a35ce87a55c
child 52566 52a0eacf04d1
--- a/src/Pure/PIDE/command.ML	Mon Jul 08 12:00:45 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 08 12:07:06 2013 +0200
@@ -252,10 +252,13 @@
 
 (* overall execution process *)
 
+fun run_print ({name, pri, print_process, ...}: print) =
+  (if Multithreading.enabled () then
+    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
+  else memo_eval) print_process;
+
 fun execute (({eval_process, ...}, prints): exec) =
- (memo_eval eval_process;
-  prints |> List.app (fn {name, pri, print_process, ...} =>
-    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
+  (memo_eval eval_process; List.app run_print prints);
 
 fun stable_goals exec_id =
   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));