# HG changeset patch
# User wenzelm
# Date 1361386637 -3600
# Node ID 19192615911ecb3958099998f83e292abf69d891
# Parent  6e40d0bb89e399c7d4fc8d22591aaa1b40564acf
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;

diff -r 6e40d0bb89e3 -r 19192615911e etc/options
--- a/etc/options	Wed Feb 20 18:04:44 2013 +0100
+++ b/etc/options	Wed Feb 20 19:57:17 2013 +0100
@@ -53,6 +53,8 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_proofs_threshold : int = 100
   -- "threshold for sub-proof parallelization"
+option parallel_proofs_reuse_timing : bool = true
+  -- "reuse timing information from old log file for parallel proof scheduling"
 
 
 section "Detail of Proof Recording"
diff -r 6e40d0bb89e3 -r 19192615911e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 20 18:04:44 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 20 19:57:17 2013 +0100
@@ -288,12 +288,14 @@
 
   object Queue
   {
-    def apply(tree: Session_Tree, get_timings: String => (List[Properties.T], Double)): Queue =
+    def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     {
       val graph = tree.graph
       val sessions = graph.keys.toList
 
-      val timings = sessions.map(name => (name, get_timings(name)))
+      val timings = sessions.map((name: String) =>
+        if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
+        else (name, (Nil, 0.0)))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =
@@ -680,7 +682,7 @@
 
     /* queue with scheduling information */
 
-    def get_timing(name: String): (List[Properties.T], Double) =
+    def load_timings(name: String): (List[Properties.T], Double) =
     {
       val (path, text) =
         find_log(name + ".gz") match {
@@ -703,7 +705,7 @@
       }
     }
 
-    val queue = Queue(selected_tree, get_timing)
+    val queue = Queue(selected_tree, load_timings)
 
 
     /* main build process */