# HG changeset patch
# User wenzelm
# Date 1612118800 -3600
# Node ID 5de4a6ae60657f8377e5f63e0c259796e7196163
# Parent  de16d797adbef88635e62a85ed4048328eb6c0a6
more parallel;

diff -r de16d797adbe -r 5de4a6ae6065 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Jan 30 20:47:00 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sun Jan 31 19:46:40 2021 +0100
@@ -458,10 +458,12 @@
           case _ => None
         }
 
-      for {
-        thy_name <- base.session_theories
-        thy_command <- Build_Job.read_theory(db_context, resources, session, thy_name.theory)
-      }
+      val read_theories =
+        Par_List.map[Document.Node.Name, Option[(Document.Node.Name, Command)]](
+          name => Build_Job.read_theory(db_context, resources, session, name.theory).map((name, _)),
+          base.session_theories)
+
+      for ((thy_name, thy_command) <- read_theories.flatten)
       yield {
         progress.expose_interrupt()
         if (verbose) progress.echo("Presenting theory " + thy_name)