afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
--- 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)))
}
}