proper options;
authorwenzelm
Tue May 21 17:55:28 2013 +0200 (2013-05-21 ago)
changeset 52104250cd2a9308d
parent 52103 fb577a13abbd
child 52105 88b423034d4f
proper options;
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/System/isabelle_process.ML	Tue May 21 17:45:53 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue May 21 17:55:28 2013 +0200
     1.3 @@ -244,8 +244,6 @@
     1.4          then Multithreading.max_threads := 2 else ();
     1.5          Goal.skip_proofs := Options.bool options "editor_skip_proofs";
     1.6          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
     1.7 -        Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
     1.8 -        Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
     1.9          tracing_messages := Options.int options "editor_tracing_messages"
    1.10        end);
    1.11  
     2.1 --- a/src/Pure/Tools/build.ML	Tue May 21 17:45:53 2013 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Tue May 21 17:55:28 2013 +0200
     2.3 @@ -106,10 +106,6 @@
     2.4      |> Unsynchronized.setmp print_mode
     2.5          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     2.6      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     2.7 -    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
     2.8 -        (Options.int options "parallel_subproofs_saturation")
     2.9 -    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
    2.10 -        (Options.real options "parallel_subproofs_threshold")
    2.11      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    2.12      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    2.13      |> Unsynchronized.setmp Future.ML_statistics true
     3.1 --- a/src/Pure/goal.ML	Tue May 21 17:45:53 2013 +0200
     3.2 +++ b/src/Pure/goal.ML	Tue May 21 17:55:28 2013 +0200
     3.3 @@ -8,8 +8,6 @@
     3.4  sig
     3.5    val skip_proofs: bool Unsynchronized.ref
     3.6    val parallel_proofs: int Unsynchronized.ref
     3.7 -  val parallel_subproofs_saturation: int Unsynchronized.ref
     3.8 -  val parallel_subproofs_threshold: real Unsynchronized.ref
     3.9    val SELECT_GOAL: tactic -> int -> tactic
    3.10    val CONJUNCTS: tactic -> int -> tactic
    3.11    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    3.12 @@ -200,8 +198,6 @@
    3.13  val skip_proofs = Unsynchronized.ref false;
    3.14  
    3.15  val parallel_proofs = Unsynchronized.ref 1;
    3.16 -val parallel_subproofs_saturation = Unsynchronized.ref 100;
    3.17 -val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
    3.18  
    3.19  fun future_enabled_level n =
    3.20    Multithreading.enabled () andalso ! parallel_proofs >= n andalso
    3.21 @@ -211,10 +207,12 @@
    3.22  
    3.23  fun future_enabled_nested n =
    3.24    future_enabled_level n andalso
    3.25 -  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
    3.26 +  forked_count () <
    3.27 +    Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value ();
    3.28  
    3.29  fun future_enabled_timing t =
    3.30 -  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
    3.31 +  future_enabled () andalso
    3.32 +    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
    3.33  
    3.34  
    3.35  (* future_result *)