src/Pure/Tools/build.scala

 
   /* queue */
 
   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 =
         Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
 

       input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
 
 
     /* 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 {
           case Some((_, path)) => (path, File.read_gzip(path))
           case None =>

           java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
         (Nil, 0.0)
       }
     }
 
-    val queue = Queue(selected_tree, get_timing)
+    val queue = Queue(selected_tree, load_timings)
 
 
     /* main build process */
 
     // prepare log dir