changeset 56875 | f6259d6fb565 |
parent 56504 | d71f4be7e287 |
child 56887 | 1ca814da47ae |
--- a/src/Pure/PIDE/command.ML Tue May 06 15:54:22 2014 +0200 +++ b/src/Pure/PIDE/command.ML Tue May 06 16:05:14 2014 +0200 @@ -399,7 +399,8 @@ local fun run_print execution_id (Print {name, delay, pri, print_process, ...}) = - if Multithreading.enabled () orelse pri <= 0 then + if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print") + then let val group = Future.worker_subgroup (); fun fork () =