# HG changeset patch
# User wenzelm
# Date 1362049772 -3600
# Node ID 7cdb86c8eb30dc56949e5771ed930da87c955b72
# Parent  30b014246e2150122a9b8cfed905ed40f92a5490
load timings in parallel for improved performance;

diff -r 30b014246e21 -r 7cdb86c8eb30 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 28 11:40:23 2013 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 28 12:09:32 2013 +0100
@@ -297,9 +297,12 @@
       val graph = tree.graph
       val sessions = graph.keys.toList
 
-      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 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(_))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =