low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
authorwenzelm
Sun, 29 Sep 2013 11:21:02 +0200
changeset 53976 da610b507799
parent 53975 22ee3fb9d596
child 53977 a7add756b9d2
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Sep 29 00:15:05 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Sep 29 11:21:02 2013 +0200
@@ -318,7 +318,7 @@
 local
 
 fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
-  if Multithreading.enabled () then
+  if Multithreading.enabled () orelse pri <= 0 then
     let
       val group = Future.worker_subgroup ();
       fun fork () =