src/Pure/Tools/build.ML
changeset 51423 e5f9a6d9ca82
parent 51399 6ac3c29a300e
child 51553 63327f679cff
     1.1 --- a/src/Pure/Tools/build.ML	Wed Mar 13 17:15:25 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Wed Mar 13 21:25:08 2013 +0100
     1.3 @@ -50,8 +50,10 @@
     1.4      |> Unsynchronized.setmp print_mode
     1.5          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     1.6      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     1.7 -    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
     1.8 -        (Options.int options "parallel_proofs_threshold")
     1.9 +    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
    1.10 +        (Options.int options "parallel_subproofs_saturation")
    1.11 +    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
    1.12 +        (Options.real options "parallel_subproofs_threshold")
    1.13      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.14      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    1.15      |> Unsynchronized.setmp Future.ML_statistics true
    1.16 @@ -99,10 +101,10 @@
    1.17        (case Symtab.lookup timings file of
    1.18          SOME offsets =>
    1.19            (case Inttab.lookup offsets offset of
    1.20 -            SOME (name', time) => if name = name' then time else Time.zeroTime
    1.21 -          | NONE => Time.zeroTime)
    1.22 -      | NONE => Time.zeroTime)
    1.23 -  | NONE => Time.zeroTime);
    1.24 +            SOME (name', time) => if name = name' then SOME time else NONE
    1.25 +          | NONE => NONE)
    1.26 +      | NONE => NONE)
    1.27 +  | NONE => NONE);
    1.28  
    1.29  in
    1.30