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 55113da610b507799
parent 55112 22ee3fb9d596
child 55114 a7add756b9d2
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
src/Pure/PIDE/command.ML
     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 () =