explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
authorwenzelm
Tue May 06 16:05:14 2014 +0200 (2014-05-06)
changeset 56875f6259d6fb565
parent 56874 5d78bce4f5a4
child 56876 f12f7c6dd83d
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
etc/options
src/Pure/PIDE/command.ML
     1.1 --- a/etc/options	Tue May 06 15:54:22 2014 +0200
     1.2 +++ b/etc/options	Tue May 06 16:05:14 2014 +0200
     1.3 @@ -63,12 +63,14 @@
     1.4    -- "additional print modes for prover output (separated by commas)"
     1.5  
     1.6  
     1.7 -section "Parallel Checking"
     1.8 +section "Parallel Processing"
     1.9  
    1.10  public option threads : int = 0
    1.11    -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.12  option threads_trace : int = 0
    1.13    -- "level of tracing information for multithreading"
    1.14 +public option parallel_print : bool = true
    1.15 +  -- "parallel and asynchronous printing of results"
    1.16  public option parallel_proofs : int = 2
    1.17    -- "level of parallel proof checking: 0, 1, 2"
    1.18  option parallel_subproofs_threshold : real = 0.01
     2.1 --- a/src/Pure/PIDE/command.ML	Tue May 06 15:54:22 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue May 06 16:05:14 2014 +0200
     2.3 @@ -399,7 +399,8 @@
     2.4  local
     2.5  
     2.6  fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
     2.7 -  if Multithreading.enabled () orelse pri <= 0 then
     2.8 +  if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
     2.9 +  then
    2.10      let
    2.11        val group = Future.worker_subgroup ();
    2.12        fun fork () =