low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
1.1 --- a/src/Pure/PIDE/command.ML Sun Sep 29 00:15:05 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Sun Sep 29 11:21:02 2013 +0200
1.3 @@ -318,7 +318,7 @@
1.4 local
1.5
1.6 fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
1.7 - if Multithreading.enabled () then
1.8 + if Multithreading.enabled () orelse pri <= 0 then
1.9 let
1.10 val group = Future.worker_subgroup ();
1.11 fun fork () =