--- a/etc/options Wed Mar 27 21:13:02 2013 +0100
+++ b/etc/options Wed Mar 27 21:25:33 2013 +0100
@@ -55,8 +55,6 @@
-- "upper bound for forks of nested proofs (multiplied by worker threads)"
option parallel_subproofs_threshold : real = 0.01
-- "lower bound of timing estimate for forked nested proofs (seconds)"
-option parallel_proofs_reuse_timing : bool = true
- -- "reuse timing information from old log file for parallel proof scheduling"
section "Detail of Proof Recording"
--- a/src/Pure/Tools/build.scala Wed Mar 27 21:13:02 2013 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 27 21:25:33 2013 +0100
@@ -326,10 +326,7 @@
val timings =
sessions.par.map((name: String) =>
- Exn.capture {
- if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
- else (name, (Nil, 0.0))
- }).toList.map(Exn.release(_))
+ Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
val command_timings =
Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
val session_timing =