# HG changeset patch
# User wenzelm
# Date 1659869939 -7200
# Node ID 0ab8a9177e41c3a9fd5323d7d823c9b184ddf173
# Parent  4827096caeb5b17dd84c7a5be39f517cb5c698ce
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;

diff -r 4827096caeb5 -r 0ab8a9177e41 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:37:57 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:58:59 2022 +0200
@@ -408,8 +408,8 @@
         case Some(entry) => entry
       }
 
-    def theory(theory: String): Theory_Context =
-      new Theory_Context(session_context, theory)
+    def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
+      new Theory_Context(session_context, theory, other_cache)
 
     def classpath(): List[File.Content_Bytes] = {
       (for {
@@ -429,9 +429,10 @@
 
   class Theory_Context private[Export](
     val session_context: Session_Context,
-    val theory: String
+    val theory: String,
+    other_cache: Option[Term.Cache]
   ) {
-    def cache: Term.Cache = session_context.cache
+    def cache: Term.Cache = other_cache getOrElse session_context.cache
 
     def get(name: String): Option[Entry] = session_context.get(theory, name)
     def apply(name: String, permissive: Boolean = false): Entry =
diff -r 4827096caeb5 -r 0ab8a9177e41 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Aug 07 12:37:57 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Aug 07 12:58:59 2022 +0200
@@ -26,13 +26,12 @@
 
   def read_session(
     session_context: Export.Session_Context,
-    progress: Progress = new Progress,
-    cache: Term.Cache = Term.Cache.make()
+    progress: Progress = new Progress
   ): Session = {
     val thys =
       for (theory <- session_context.theory_names()) yield {
         progress.echo("Reading theory " + theory)
-        read_theory(session_context.theory(theory), cache = cache)
+        read_theory(session_context.theory(theory))
       }
 
     val graph0 =
@@ -110,9 +109,9 @@
 
   def read_theory(
     theory_context: Export.Theory_Context,
-    permissive: Boolean = false,
-    cache: Term.Cache = Term.Cache.none
+    permissive: Boolean = false
   ): Theory = {
+    val cache = theory_context.cache
     val session_name = theory_context.session_context.session_name
     val theory_name = theory_context.theory
     read_theory_parents(theory_context) match {
@@ -374,9 +373,11 @@
   def read_proof(
     session_context: Export.Session_Context,
     id: Thm_Id,
-    cache: Term.Cache = Term.Cache.none
+    other_cache: Option[Term.Cache] = None
   ): Option[Proof] = {
-    val theory_context = session_context.theory(id.theory_name)
+    val theory_context = session_context.theory(id.theory_name, other_cache = other_cache)
+    val cache = theory_context.cache
+
     for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
     yield {
       val body = entry.uncompressed_yxml
@@ -398,7 +399,7 @@
     session_context: Export.Session_Context,
     proof: Term.Proof,
     suppress: Thm_Id => Boolean = _ => false,
-    cache: Term.Cache = Term.Cache.none
+    other_cache: Option[Term.Cache] = None
   ): List[(Thm_Id, Proof)] = {
     var seen = Set.empty[Long]
     var result = SortedMap.empty[Long, (Thm_Id, Proof)]
@@ -413,7 +414,7 @@
           seen += thm.serial
           val id = Thm_Id(thm.serial, thm.theory_name)
           if (!suppress(id)) {
-            Export_Theory.read_proof(session_context, id, cache = cache) match {
+            Export_Theory.read_proof(session_context, id, other_cache = other_cache) match {
               case Some(p) =>
                 result += (thm.serial -> (id -> p))
                 boxes(Some((thm.serial, p.proof)), p.proof)
diff -r 4827096caeb5 -r 0ab8a9177e41 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sun Aug 07 12:37:57 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sun Aug 07 12:58:59 2022 +0200
@@ -134,10 +134,9 @@
           { case (session, thys) =>
               using(open_session(session)) { session_context =>
                 for (thy_name <- thys) yield {
-                  val theory_context = session_context.theory(thy_name)
-                  val theory =
-                    Export_Theory.read_theory(theory_context,
-                      permissive = true, cache = session_context.cache)
+                  val theory_context =
+                    session_context.theory(thy_name, other_cache = Some(Term.Cache.none))
+                  val theory = Export_Theory.read_theory(theory_context, permissive = true)
                   thy_name -> Node_Info.make(theory)
                 }
               }