# HG changeset patch
# User wenzelm
# Date 1361993781 -3600
# Node ID ec7f10155389b054d0a6eced973985b1bed1ed23
# Parent  d9f3d91208afc666d802e61343615b7b8c977614
parallel dep.load_files saves approx. 1s on 4 cores;

diff -r d9f3d91208af -r ec7f10155389 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Wed Feb 27 19:39:16 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Wed Feb 27 20:36:21 2013 +0100
@@ -65,10 +65,13 @@
 
     def load_files: List[Path] =
     {
-      // FIXME par.map (!?)
-      ((Nil: List[Path]) /: rev_deps) {
-        case (files, dep) =>
-          dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a)) ::: files
+      val dep_files =
+        rev_deps.par.map(dep =>
+          Exn.capture {
+            dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a))
+          }).toList
+      ((Nil: List[Path]) /: dep_files) {
+        case (acc_files, files) => Exn.release(files) ::: acc_files
       }
     }
   }