# HG changeset patch
# User wenzelm
# Date 1369151728 -7200
# Node ID 250cd2a9308dbeee8c4ba71f36ae2c5386423694
# Parent  fb577a13abbdb513ee4c8bdf0d9b2bf3a9b14a62
proper options;

diff -r fb577a13abbd -r 250cd2a9308d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue May 21 17:45:53 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue May 21 17:55:28 2013 +0200
@@ -244,8 +244,6 @@
         then Multithreading.max_threads := 2 else ();
         Goal.skip_proofs := Options.bool options "editor_skip_proofs";
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
-        Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
-        Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
         tracing_messages := Options.int options "editor_tracing_messages"
       end);
 
diff -r fb577a13abbd -r 250cd2a9308d src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue May 21 17:45:53 2013 +0200
+++ b/src/Pure/Tools/build.ML	Tue May 21 17:55:28 2013 +0200
@@ -106,10 +106,6 @@
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
-        (Options.int options "parallel_subproofs_saturation")
-    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
-        (Options.real options "parallel_subproofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
diff -r fb577a13abbd -r 250cd2a9308d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue May 21 17:45:53 2013 +0200
+++ b/src/Pure/goal.ML	Tue May 21 17:55:28 2013 +0200
@@ -8,8 +8,6 @@
 sig
   val skip_proofs: bool Unsynchronized.ref
   val parallel_proofs: int Unsynchronized.ref
-  val parallel_subproofs_saturation: int Unsynchronized.ref
-  val parallel_subproofs_threshold: real Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -200,8 +198,6 @@
 val skip_proofs = Unsynchronized.ref false;
 
 val parallel_proofs = Unsynchronized.ref 1;
-val parallel_subproofs_saturation = Unsynchronized.ref 100;
-val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
 
 fun future_enabled_level n =
   Multithreading.enabled () andalso ! parallel_proofs >= n andalso
@@ -211,10 +207,12 @@
 
 fun future_enabled_nested n =
   future_enabled_level n andalso
-  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
+  forked_count () <
+    Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value ();
 
 fun future_enabled_timing t =
-  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
+  future_enabled () andalso
+    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
 
 
 (* future_result *)