# HG changeset patch
# User wenzelm
# Date 1637094075 -3600
# Node ID 507f50dbeb799cdaf12de61e134c9752dae6e26c
# Parent  1c2863734db1a968097ab83b35a959877e9fb9f1
just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);

diff -r 1c2863734db1 -r 507f50dbeb79 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Nov 16 18:45:31 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Tue Nov 16 21:21:15 2021 +0100
@@ -35,31 +35,6 @@
       theory_path(name).dir + Path.explode("files") + path.squash.html
 
 
-    /* cached theory exports */
-
-    val cache: Term.Cache = Term.Cache.make()
-
-    private val already_presented = Synchronized(Set.empty[String])
-    def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
-      already_presented.change_result(presented =>
-        (nodes.filterNot(name => presented.contains(name.theory)),
-          presented ++ nodes.iterator.map(_.theory)))
-
-    private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
-    def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
-    {
-      theory_cache.change_result(thys =>
-      {
-        thys.get(thy_name) match {
-          case Some(thy) => (thy, thys)
-          case None =>
-            val thy = make_thy
-            (thy, thys + (thy_name -> thy))
-        }
-      })
-    }
-
-
     /* HTML content */
 
     def head(title: String, rest: XML.Body = Nil): XML.Tree =
@@ -89,6 +64,40 @@
   }
 
 
+  /* presentation state */
+
+  class State
+  {
+    /* already presented theories */
+
+    private val already_presented = Synchronized(Set.empty[String])
+
+    def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
+      already_presented.change_result(presented =>
+        (nodes.filterNot(name => presented.contains(name.theory)),
+          presented ++ nodes.iterator.map(_.theory)))
+
+
+    /* cached theory exports */
+
+    val cache: Term.Cache = Term.Cache.make()
+
+    private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
+    def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
+    {
+      theory_cache.change_result(thys =>
+      {
+        thys.get(thy_name) match {
+          case Some(thy) => (thy, thys)
+          case None =>
+            val thy = make_thy
+            (thy, thys + (thy_name -> thy))
+        }
+      })
+    }
+  }
+
+
   /* presentation elements */
 
   sealed case class Elements(
@@ -495,6 +504,7 @@
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
+    state: State,
     session_elements: Elements): Unit =
   {
     val info = deps.sessions_structure(session)
@@ -547,12 +557,12 @@
         val theory =
           if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
           else {
-            html_context.cache_theory(thy_name,
+            state.cache_theory(thy_name,
               {
                 val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
                 if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
                   Export_Theory.read_theory(
-                    provider, session, thy_name, cache = html_context.cache)
+                    provider, session, thy_name, cache = state.cache)
                 }
                 else Export_Theory.no_theory
               })
@@ -645,7 +655,7 @@
       })
     }
 
-    val theories = html_context.register_presented(hierarchy_theories).flatMap(present_theory)
+    val theories = state.register_presented(hierarchy_theories).flatMap(present_theory)
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
diff -r 1c2863734db1 -r 507f50dbeb79 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 16 18:45:31 2021 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 16 21:21:15 2021 +0100
@@ -506,6 +506,8 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
+        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)) {
             progress.expose_interrupt()
@@ -513,14 +515,13 @@
 
             val html_context =
               new Presentation.HTML_Context {
-                override val cache: Term.Cache = store.cache
                 override def root_dir: Path = presentation_dir
                 override def theory_session(name: Document.Node.Name): Sessions.Info =
                   deps.sessions_structure(deps(session).theory_qualifier(name))
               }
             Presentation.session_html(
               session, deps, db_context, progress = progress,
-              verbose = verbose, html_context = html_context,
+              verbose = verbose, html_context = html_context, state = state,
               Presentation.elements1)
           })
       }