# HG changeset patch
# User wenzelm
# Date 1637160851 -3600
# Node ID cfc15da73a78a34ea7de234a05ffc1add17fa0f2
# Parent  79fa9f2d02fa6cfc66192b6354c11ccc130a9851
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);

diff -r 79fa9f2d02fa -r cfc15da73a78 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)))
       }
     }