--- 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)