# HG changeset patch
# User wenzelm
# Date 1399385114 -7200
# Node ID f6259d6fb5657ae186c395f68e6c014ae01af97e
# Parent  5d78bce4f5a4d7466614caebde476b2a4d50703e
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";

diff -r 5d78bce4f5a4 -r f6259d6fb565 etc/options
--- a/etc/options	Tue May 06 15:54:22 2014 +0200
+++ b/etc/options	Tue May 06 16:05:14 2014 +0200
@@ -63,12 +63,14 @@
   -- "additional print modes for prover output (separated by commas)"
 
 
-section "Parallel Checking"
+section "Parallel Processing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
+public option parallel_print : bool = true
+  -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 2
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
diff -r 5d78bce4f5a4 -r f6259d6fb565 src/Pure/PIDE/command.ML
--- 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 () =