# HG changeset patch
# User wenzelm
# Date 1636371935 -3600
# Node ID 161e84e6b40acf630bcdc9a7f2cac8509c5e9c49
# Parent  25f5f1fa31bb7a9a1e4b8da3d65ee0c15670dad3
just one cache, via HTML_Context, via Sessions.Store or Session;

diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/PIDE/session.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -127,7 +127,7 @@
 {
   session =>
 
-  val cache: XML.Cache = XML.Cache.make()
+  val cache: Term.Cache = Term.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/PIDE/xml.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -199,15 +199,15 @@
   object Cache
   {
     def make(
-      xz: XZ.Cache = XZ.Cache.make(),
-      max_string: Int = isabelle.Cache.default_max_string,
+        xz: XZ.Cache = XZ.Cache.make(),
+        max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
       new Cache(xz, max_string, initial_size)
 
     val none: Cache = make(XZ.Cache.none, max_string = 0)
   }
 
-  class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int)
+  class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
     extends isabelle.Cache(max_string, initial_size)
   {
     protected def cache_props(x: Properties.T): Properties.T =
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/Thy/presentation.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -20,12 +20,11 @@
 
   sealed case class HTML_Document(title: String, content: String)
 
-  def html_context(): HTML_Context = new HTML_Context
+  def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
+    new HTML_Context(cache)
 
-  final class HTML_Context private[Presentation]
+  final class HTML_Context private[Presentation](val cache: Term.Cache)
   {
-    val term_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 =>
@@ -446,7 +445,7 @@
                 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.term_cache)
+                    provider, session, thy_name, cache = html_context.cache)
                 }
                 else Export_Theory.no_theory
               })
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/Thy/sessions.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -1212,7 +1212,7 @@
     val store: Sessions.Store,
     database_server: Option[SQL.Database]) extends AutoCloseable
   {
-    def cache: XML.Cache = store.cache
+    def cache: Term.Cache = store.cache
 
     def close(): Unit = database_server.foreach(_.close())
 
@@ -1267,10 +1267,10 @@
     }
   }
 
-  def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+  def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
-  class Store private[Sessions](val options: Options, val cache: XML.Cache)
+  class Store private[Sessions](val options: Options, val cache: Term.Cache)
   {
     store =>
 
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/Tools/build.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -507,7 +507,7 @@
         }
 
         val resources = Resources.empty
-        val html_context = Presentation.html_context()
+        val html_context = Presentation.html_context(cache = store.cache)
 
         using(store.open_database_context())(db_context =>
           for (info <- presentation_sessions) {
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/Tools/build_job.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -241,7 +241,7 @@
         new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
-          override val cache: XML.Cache = store.cache
+          override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
           {
diff -r 25f5f1fa31bb -r 161e84e6b40a src/Pure/term.scala
--- a/src/Pure/term.scala	Mon Nov 08 09:31:26 2021 +0000
+++ b/src/Pure/term.scala	Mon Nov 08 12:45:35 2021 +0100
@@ -200,15 +200,16 @@
   object Cache
   {
     def make(
+        xz: XZ.Cache = XZ.Cache.make(),
         max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
-      new Cache(initial_size, max_string)
+      new Cache(xz, initial_size, max_string)
 
     val none: Cache = make(max_string = 0)
   }
 
-  class Cache private[Term](max_string: Int, initial_size: Int)
-    extends isabelle.Cache(max_string, initial_size)
+  class Cache(xz: XZ.Cache, max_string: Int, initial_size: Int)
+    extends XML.Cache(xz, max_string, initial_size)
   {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))