afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
authorwenzelm
Wed, 17 Nov 2021 15:54:11 +0100
changeset 74815 cfc15da73a78
parent 74814 79fa9f2d02fa
child 74816 1e7bb95c75e7
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 17 15:46:35 2021 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 17 15:54:11 2021 +0100
@@ -509,7 +509,8 @@
         val state = new Presentation.State { override val cache: Term.Cache = store.cache }
 
         using(store.open_database_context())(db_context =>
-          for (session <- presentation_sessions.map(_.name)) {
+          Par_List.map((session: String) =>
+          {
             progress.expose_interrupt()
             progress.echo("Presenting " + session + " ...")
 
@@ -523,7 +524,7 @@
               session, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context, state = state,
               Presentation.elements1)
-          })
+          }, presentation_sessions.map(_.name)))
       }
     }