src/Pure/PIDE/command.ML
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 () =