# HG changeset patch
# User wenzelm
# Date 1636110690 -3600
# Node ID c492c8efcab474daf3337dd54885967b090ac1c6
# Parent  0554a5c4c191339a50a1e63b00b45c8681958d86
clarified HTML_Context: just one context type;

diff -r 0554a5c4c191 -r c492c8efcab4 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 12:05:17 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 12:11:30 2021 +0100
@@ -27,6 +27,21 @@
 
   final class HTML_Context private[Presentation](fonts_url: String => String)
   {
+    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))
+        }
+      })
+    }
+
     def init_fonts(dir: Path): Unit =
     {
       val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
@@ -328,32 +343,6 @@
   }
 
 
-  /* theory cache */
-
-  object Theory_Cache
-  {
-    def apply(): Theory_Cache = new Theory_Cache()
-  }
-
-  class Theory_Cache private()
-  {
-    private val cache = Synchronized(Map.empty[String, Export_Theory.Theory])
-
-    def apply(thy_name: String, make_thy: => Export_Theory.Theory): Export_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))
-        }
-      })
-    }
-  }
-
-
   /* present session */
 
   val session_graph_path = Path.explode("session_graph.pdf")
@@ -402,8 +391,7 @@
     verbose: Boolean = false,
     html_context: HTML_Context,
     elements: Elements,
-    presentation: Context,
-    theory_cache: Theory_Cache = Theory_Cache()): Unit =
+    presentation: Context): Unit =
   {
     val info = deps.sessions_structure(session)
     val options = info.options
@@ -449,7 +437,7 @@
     def read_theory(thy_name: String): Export_Theory.Theory =
       if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
       else {
-        theory_cache(thy_name,
+        html_context.cache_theory(thy_name,
           {
             val qualifier = deps(session).theory_qualifier(thy_name)
             val provider = Export.Provider.database_context(db_context, List(qualifier), thy_name)
diff -r 0554a5c4c191 -r c492c8efcab4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Nov 05 12:05:17 2021 +0100
+++ b/src/Pure/Tools/build.scala	Fri Nov 05 12:11:30 2021 +0100
@@ -501,7 +501,6 @@
 
         val resources = Resources.empty
         val html_context = Presentation.html_context()
-        val theory_cache = Presentation.Theory_Cache()
 
         using(store.open_database_context())(db_context =>
           for ((_, (session_name, _)) <- presentation_chapters) {
@@ -510,8 +509,7 @@
             Presentation.session_html(
               resources, session_name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
-              elements = Presentation.elements1, presentation = presentation,
-              theory_cache = theory_cache)
+              elements = Presentation.elements1, presentation = presentation)
           })
 
         val browser_chapters =