test-tuned;

--- a/src/Pure/Thy/presentation.scala	Tue Sep 28 11:30:14 2021 +0200
+++ b/src/Pure/Thy/presentation.scala	Tue Sep 28 13:55:39 2021 +0200
@@ -423,7 +423,8 @@
     verbose: Boolean = false,
     html_context: HTML_Context,
     elements: Elements,
-    presentation: Context): Unit =
+    presentation: Context,
+    cache: mutable.Map[Document.Node.Name, Seq[Export_Theory.Entity[Export_Theory.No_Content]]] = mutable.Map.empty[Document.Node.Name, Seq[Export_Theory.Entity[Export_Theory.No_Content]]]): Unit =
   {
     val info = deps.sessions_structure(session)
     val options = info.options
@@ -466,22 +467,24 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
-    def read_exports(name: Document.Node.Name) =
+    def read_exports(name: Document.Node.Name): Iterable[Export_Theory.Entity[Export_Theory.No_Content]] =
     {
-      if (Sessions.is_pure(name.theory_base_name)) {
-        Vector.empty
-      } else {
-        val session1 = deps(session).theory_qualifier(name)
-        val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
-        provider(Export.THEORY_PREFIX + "parents") match {
-          case Some(_) =>
-            val theory = Export_Theory.read_theory(provider, session1, name.theory)
-            theory.entity_iterator.toVector
-          case None =>
-            progress.echo_error_message("No exports for: " + name)
-            Vector.empty
+      cache.getOrElseUpdate(name, {
+        if (Sessions.is_pure(name.theory_base_name)) {
+          Vector.empty
+        } else {
+          val session1 = deps(session).theory_qualifier(name)
+          val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
+          provider(Export.THEORY_PREFIX + "parents") match {
+            case Some(_) =>
+              val theory = Export_Theory.read_theory(provider, session1, name.theory)
+              theory.entity_iterator.toVector
+            case None =>
+              progress.echo_error_message("No exports for: " + name)
+              Vector.empty
+          }
         }
-      }
+      })
     }
 
     val exports = base.known_theories.map(_._2.name).map(node => node -> read_exports(node)).toMap

--- a/src/Pure/Tools/build.scala	Tue Sep 28 11:30:14 2021 +0200
+++ b/src/Pure/Tools/build.scala	Tue Sep 28 13:55:39 2021 +0200
@@ -10,6 +10,7 @@
 
 import scala.collection.immutable.SortedSet
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 
 object Build
@@ -502,6 +503,8 @@
         val resources = Resources.empty
         val html_context = Presentation.html_context()
 
+        val cached_nodes = mutable.Map.empty[Document.Node.Name, Seq[Export_Theory.Entity[Export_Theory.No_Content]]]
+
         using(store.open_database_context())(db_context =>
           for ((_, (session_name, _)) <- presentation_chapters) {
             progress.expose_interrupt()
@@ -509,7 +512,7 @@
             Presentation.session_html(
               resources, session_name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
-              elements = Presentation.elements1, presentation = presentation)
+              elements = Presentation.elements1, presentation = presentation, cache = cached_nodes)
           })
 
         val browser_chapters =