# HG changeset patch
# User wenzelm
# Date 1659732565 -7200
# Node ID efc25bf4b795f9b8b0523cc6d790399de075104a
# Parent  11b2bf6f90d81ca7ffb9d16a093aaead7aaa85a3
discontinued Export.Provider in favour of Export.Context and its derivatives;
uniform treatment of all sessions, including Pure;

diff -r 11b2bf6f90d8 -r efc25bf4b795 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 21:29:25 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 22:49:25 2022 +0200
@@ -256,88 +256,6 @@
   }
 
 
-  /* abstract provider */
-
-  object Provider {
-    private def database_provider(
-        db: SQL.Database,
-        cache: XML.Cache,
-        session: String,
-        theory: String,
-        _theory_names: Synchronized[Option[List[String]]]
-    ): Provider = {
-      new Provider {
-        override def theory_names: List[String] =
-          _theory_names.change_result { st =>
-            val res = st.getOrElse(read_theory_names(db, session))
-            (res, Some(res))
-          }
-
-        override def apply(export_name: String): Option[Entry] =
-          if (theory.isEmpty) None
-          else {
-            Entry_Name(session = session, theory = theory, name = export_name)
-              .read(db, cache)
-          }
-
-        override def focus(other_theory: String): Provider =
-          if (other_theory == theory) this
-          else database_provider(db, cache, session, theory, _theory_names)
-
-        override def toString: String = db.toString
-      }
-    }
-
-    def database(
-      db: SQL.Database,
-      cache: XML.Cache,
-      session: String,
-      theory: String = ""
-    ): Provider = database_provider(db, cache, session, theory, Synchronized(None))
-
-    def snapshot(
-      resources: Resources,
-      snapshot: Document.Snapshot
-    ): Provider =
-      new Provider {
-        override def theory_names: List[String] =
-          (for {
-            (name, _) <- snapshot.version.nodes.iterator
-            if name.is_theory && !resources.session_base.loaded_theory(name)
-          } yield name.theory).toList
-
-        override def apply(name: String): Option[Entry] =
-          snapshot.all_exports.get(
-            Entry_Name(session = Sessions.DRAFT, theory = snapshot.node_name.theory, name = name))
-
-        override def focus(other_theory: String): Provider =
-          if (other_theory == snapshot.node_name.theory) this
-          else {
-            val node_name =
-              snapshot.version.nodes.theory_name(other_theory) getOrElse
-                error("Bad theory " + quote(other_theory))
-            Provider.snapshot(resources, snapshot.state.snapshot(node_name))
-          }
-
-        override def toString: String = snapshot.toString
-      }
-  }
-
-  trait Provider {
-    def theory_names: List[String]
-
-    def apply(export_name: String): Option[Entry]
-
-    def uncompressed_yxml(export_name: String): XML.Body =
-      apply(export_name) match {
-        case Some(entry) => entry.uncompressed_yxml
-        case None => Nil
-      }
-
-    def focus(other_theory: String): Provider
-  }
-
-
   /* context for retrieval */
 
   def context(db_context: Sessions.Database_Context): Context = new Context(db_context)
@@ -473,11 +391,20 @@
       "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }
 
-  class Theory_Context private[Export](val session_context: Session_Context, theory: String) {
+  class Theory_Context private[Export](
+    val session_context: Session_Context,
+    val theory: String
+  ) {
     def get(name: String): Option[Entry] = session_context.get(theory, name)
     def apply(name: String, permissive: Boolean = false): Entry =
       session_context.apply(theory, name, permissive = permissive)
 
+    def uncompressed_yxml(name: String): XML.Body =
+      get(name) match {
+        case Some(entry) => entry.uncompressed_yxml
+        case None => Nil
+      }
+
     override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
   }
 
diff -r 11b2bf6f90d8 -r efc25bf4b795 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 05 21:29:25 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 05 22:49:25 2022 +0200
@@ -25,21 +25,15 @@
   }
 
   def read_session(
-    store: Sessions.Store,
-    sessions_structure: Sessions.Structure,
-    session_name: String,
+    session_context: Export.Session_Context,
     progress: Progress = new Progress,
-    cache: Term.Cache = Term.Cache.make()): Session = {
+    cache: Term.Cache = Term.Cache.make()
+  ): Session = {
     val thys =
-      sessions_structure.build_requirements(List(session_name)).flatMap(session =>
-        using(store.open_database(session)) { db =>
-          val provider = Export.Provider.database(db, store.cache, session)
-          for (theory <- provider.theory_names)
-          yield {
-            progress.echo("Reading theory " + theory)
-            read_theory(provider, session, theory, cache = cache)
-          }
-        })
+      for (theory <- session_context.theory_names()) yield {
+        progress.echo("Reading theory " + theory)
+        read_theory(session_context.theory(theory), cache = cache)
+      }
 
     val graph0 =
       thys.foldLeft(Graph.string[Option[Theory]]) {
@@ -53,7 +47,7 @@
           }
       }
 
-    Session(session_name, graph1)
+    Session(session_context.session_name, graph1)
   }
 
 
@@ -107,63 +101,45 @@
         (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap)
   }
 
-  def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] =
-    provider.focus(theory_name)(Export.THEORY_PARENTS)
+  def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
+    theory_context.get(Export.THEORY_PARENTS)
       .map(entry => Library.trim_split_lines(entry.uncompressed.text))
 
   def no_theory: Theory =
     Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
 
   def read_theory(
-    provider: Export.Provider,
-    session_name: String,
-    theory_name: String,
+    theory_context: Export.Theory_Context,
     permissive: Boolean = false,
     cache: Term.Cache = Term.Cache.none
   ): Theory = {
-    val theory_provider = provider.focus(theory_name)
-    read_theory_parents(theory_provider, theory_name) match {
+    val session_name = theory_context.session_context.session_name
+    val theory_name = theory_context.theory
+    read_theory_parents(theory_context) match {
       case None if permissive => no_theory
       case None =>
         error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name))
       case Some(parents) =>
         val theory =
           Theory(theory_name, parents,
-            read_types(theory_provider),
-            read_consts(theory_provider),
-            read_axioms(theory_provider),
-            read_thms(theory_provider),
-            read_classes(theory_provider),
-            read_locales(theory_provider),
-            read_locale_dependencies(theory_provider),
-            read_classrel(theory_provider),
-            read_arities(theory_provider),
-            read_constdefs(theory_provider),
-            read_typedefs(theory_provider),
-            read_datatypes(theory_provider),
-            read_spec_rules(theory_provider),
-            read_others(theory_provider))
+            read_types(theory_context),
+            read_consts(theory_context),
+            read_axioms(theory_context),
+            read_thms(theory_context),
+            read_classes(theory_context),
+            read_locales(theory_context),
+            read_locale_dependencies(theory_context),
+            read_classrel(theory_context),
+            read_arities(theory_context),
+            read_constdefs(theory_context),
+            read_typedefs(theory_context),
+            read_datatypes(theory_context),
+            read_spec_rules(theory_context),
+            read_others(theory_context))
         if (cache.no_cache) theory else theory.cache(cache)
     }
   }
 
-  def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = {
-    val session_name = Thy_Header.PURE
-    val theory_name = Thy_Header.PURE
-
-    using(store.open_database(session_name)) { db =>
-      val provider = Export.Provider.database(db, store.cache, session_name)
-      read(provider, session_name, theory_name)
-    }
-  }
-
-  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory =
-    read_pure(store, read_theory(_, _, _, cache = cache))
-
-  def read_pure_proof(
-      store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] =
-    read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
-
 
   /* entities */
 
@@ -225,7 +201,7 @@
   type Entity0 = Entity[No_Content]
 
   def read_entities[A <: Content[A]](
-    provider: Export.Provider,
+    theory_context: Export.Theory_Context,
     export_name: String,
     kind: String,
     decode: XML.Decode.T[A]
@@ -245,7 +221,7 @@
         case _ => err()
       }
     }
-    provider.uncompressed_yxml(export_name).map(decode_entity)
+    theory_context.uncompressed_yxml(export_name).map(decode_entity)
   }
 
 
@@ -281,8 +257,8 @@
         abbrev.map(cache.typ))
   }
 
-  def read_types(provider: Export.Provider): List[Entity[Type]] =
-    read_entities(provider, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME,
+  def read_types(theory_context: Export.Theory_Context): List[Entity[Type]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME,
       { body =>
         import XML.Decode._
         val (syntax, args, abbrev) =
@@ -309,8 +285,8 @@
         propositional)
   }
 
-  def read_consts(provider: Export.Provider): List[Entity[Const]] =
-    read_entities(provider, Export.THEORY_PREFIX + "consts", Markup.CONSTANT,
+  def read_consts(theory_context: Export.Theory_Context): List[Entity[Const]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "consts", Markup.CONSTANT,
       { body =>
         import XML.Decode._
         val (syntax, (typargs, (typ, (abbrev, propositional)))) =
@@ -349,16 +325,14 @@
     override def cache(cache: Term.Cache): Axiom = Axiom(prop.cache(cache))
   }
 
-  def read_axioms(provider: Export.Provider): List[Entity[Axiom]] =
-    read_entities(provider, Export.THEORY_PREFIX + "axioms", Markup.AXIOM,
+  def read_axioms(theory_context: Export.Theory_Context): List[Entity[Axiom]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "axioms", Markup.AXIOM,
       body => Axiom(decode_prop(body)))
 
 
   /* theorems */
 
-  sealed case class Thm_Id(serial: Long, theory_name: String) {
-    def pure: Boolean = theory_name == Thy_Header.PURE
-  }
+  sealed case class Thm_Id(serial: Long, theory_name: String)
 
   sealed case class Thm(
     prop: Prop,
@@ -372,8 +346,8 @@
         cache.proof(proof))
   }
 
-  def read_thms(provider: Export.Provider): List[Entity[Thm]] =
-    read_entities(provider, Export.THEORY_PREFIX + "thms", Kind.THM,
+  def read_thms(theory_context: Export.Theory_Context): List[Entity[Thm]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "thms", Kind.THM,
       { body =>
         import XML.Decode._
         import Term_XML.Decode._
@@ -398,11 +372,12 @@
   }
 
   def read_proof(
-    provider: Export.Provider,
+    session_context: Export.Session_Context,
     id: Thm_Id,
     cache: Term.Cache = Term.Cache.none
   ): Option[Proof] = {
-    for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
+    val theory_context = session_context.theory(id.theory_name)
+    for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
     yield {
       val body = entry.uncompressed_yxml
       val (typargs, (args, (prop_body, proof_body))) = {
@@ -420,8 +395,7 @@
   }
 
   def read_proof_boxes(
-    store: Sessions.Store,
-    provider: Export.Provider,
+    session_context: Export.Session_Context,
     proof: Term.Proof,
     suppress: Thm_Id => Boolean = _ => false,
     cache: Term.Cache = Term.Cache.none
@@ -439,10 +413,7 @@
           seen += thm.serial
           val id = Thm_Id(thm.serial, thm.theory_name)
           if (!suppress(id)) {
-            val read =
-              if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache)
-              else Export_Theory.read_proof(provider, id, cache = cache)
-            read match {
+            Export_Theory.read_proof(session_context, id, cache = cache) match {
               case Some(p) =>
                 result += (thm.serial -> (id -> p))
                 boxes(Some((thm.serial, p.proof)), p.proof)
@@ -473,8 +444,8 @@
         axioms.map(_.cache(cache)))
   }
 
-  def read_classes(provider: Export.Provider): List[Entity[Class]] =
-    read_entities(provider, Export.THEORY_PREFIX + "classes", Markup.CLASS,
+  def read_classes(theory_context: Export.Theory_Context): List[Entity[Class]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "classes", Markup.CLASS,
       { body =>
         import XML.Decode._
         import Term_XML.Decode._
@@ -497,8 +468,8 @@
         axioms.map(_.cache(cache)))
   }
 
-  def read_locales(provider: Export.Provider): List[Entity[Locale]] =
-    read_entities(provider, Export.THEORY_PREFIX + "locales", Markup.LOCALE,
+  def read_locales(theory_context: Export.Theory_Context): List[Entity[Locale]] =
+    read_entities(theory_context, Export.THEORY_PREFIX + "locales", Markup.LOCALE,
       { body =>
         import XML.Decode._
         import Term_XML.Decode._
@@ -530,8 +501,11 @@
       subst_types.isEmpty && subst_terms.isEmpty
   }
 
-  def read_locale_dependencies(provider: Export.Provider): List[Entity[Locale_Dependency]] =
-    read_entities(provider, Export.THEORY_PREFIX + "locale_dependencies", Kind.LOCALE_DEPENDENCY,
+  def read_locale_dependencies(
+    theory_context: Export.Theory_Context
+  ): List[Entity[Locale_Dependency]] = {
+    read_entities(theory_context, Export.THEORY_PREFIX + "locale_dependencies",
+      Kind.LOCALE_DEPENDENCY,
       { body =>
         import XML.Decode._
         import Term_XML.Decode._
@@ -540,6 +514,7 @@
             pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
         Locale_Dependency(source, target, prefix, subst_types, subst_terms)
       })
+  }
 
 
   /* sort algebra */
@@ -549,8 +524,8 @@
       Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
   }
 
-  def read_classrel(provider: Export.Provider): List[Classrel] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
+  def read_classrel(theory_context: Export.Theory_Context): List[Classrel] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
     val classrel = {
       import XML.Decode._
       list(pair(decode_prop, pair(string, string)))(body)
@@ -569,8 +544,8 @@
         prop.cache(cache))
   }
 
-  def read_arities(provider: Export.Provider): List[Arity] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
+  def read_arities(theory_context: Export.Theory_Context): List[Arity] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
     val arities = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -587,8 +562,8 @@
       Constdef(cache.string(name), cache.string(axiom_name))
   }
 
-  def read_constdefs(provider: Export.Provider): List[Constdef] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
+  def read_constdefs(theory_context: Export.Theory_Context): List[Constdef] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
     val constdefs = {
       import XML.Decode._
       list(pair(string, string))(body)
@@ -616,8 +591,8 @@
         cache.string(axiom_name))
   }
 
-  def read_typedefs(provider: Export.Provider): List[Typedef] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
+  def read_typedefs(theory_context: Export.Theory_Context): List[Typedef] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
     val typedefs = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -650,8 +625,8 @@
         constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }))
   }
 
-  def read_datatypes(provider: Export.Provider): List[Datatype] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
+  def read_datatypes(theory_context: Export.Theory_Context): List[Datatype] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
     val datatypes = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -740,8 +715,8 @@
         rules.map(cache.term))
   }
 
-  def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = {
-    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
+  def read_spec_rules(theory_context: Export.Theory_Context): List[Spec_Rule] = {
+    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
     val spec_rules = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -761,15 +736,15 @@
     override def cache(cache: Term.Cache): Other = this
   }
 
-  def read_others(provider: Export.Provider): Map[String, List[Entity[Other]]] = {
+  def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
     val kinds =
-      provider(Export.THEORY_PREFIX + "other_kinds") match {
+      theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
         case Some(entry) => split_lines(entry.uncompressed.text)
         case None => Nil
       }
     val other = Other()
     def read_other(kind: String): List[Entity[Other]] =
-      read_entities(provider, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other)
+      read_entities(theory_context, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other)
 
     kinds.map(kind => kind -> read_other(kind)).toMap
   }
diff -r 11b2bf6f90d8 -r efc25bf4b795 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 05 21:29:25 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 05 22:49:25 2022 +0200
@@ -117,6 +117,8 @@
       deps: Sessions.Deps,
       db_context: Sessions.Database_Context
     ): Nodes = {
+      val export_context = Export.context(db_context)
+
       type Batch = (String, List[String])
       val batches =
         presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))(
@@ -124,43 +126,35 @@
               val thys = deps(session).loaded_theories.keys.filterNot(seen)
               (seen ++ thys, (session, thys) :: batches)
           })._2
+
       val theory_node_info =
         Par_List.map[Batch, List[(String, Node_Info)]](
           { case (session, thys) =>
-              db_context.database(session) { db =>
-                val provider = Export.Provider.database(db, db_context.cache, session)
-                val result =
-                  for (thy_name <- thys) yield {
-                    val theory =
-                      if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
-                      else {
-                        Export_Theory.read_theory(provider, session, thy_name,
-                          permissive = true, cache = db_context.cache)
-                      }
-                    thy_name -> Node_Info.make(theory)
-                  }
-                Some(result)
-              } getOrElse Nil
+              using(export_context.open_session(deps.base_info(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 = db_context.cache)
+                  thy_name -> Node_Info.make(theory)
+                }
+              }
           }, batches).flatten.toMap
+
       val files_info =
         deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session =>
-          db_context.database(session) { db =>
-            val res =
-              Export.read_theory_names(db, session).flatMap { theory =>
-                val files =
-                  Export.read_files(name =>
-                    Export.Entry_Name(session = session, theory = theory, name = name)
-                      .read(db, db_context.cache)
-                      .getOrElse(Export.empty_entry(theory, name)))
-                files match {
-                  case None => Nil
-                  case Some((thy, other)) =>
-                    val thy_file_info = File_Info(theory, is_theory = true)
-                    (thy -> thy_file_info) :: other.map(_ -> File_Info(theory))
-                }
+          using(export_context.open_session(deps.base_info(session))) { session_context =>
+            session_context.theory_names().flatMap { theory =>
+              val theory_context = session_context.theory(theory)
+              Export.read_files(theory_context(_, permissive = true)) match {
+                case None => Nil
+                case Some((thy, other)) =>
+                  val thy_file_info = File_Info(theory, is_theory = true)
+                  (thy -> thy_file_info) :: other.map(_ -> File_Info(theory))
               }
-            Some(res)
-          }.getOrElse(Nil)).toMap
+            }
+          }).toMap
+
       new Nodes(theory_node_info, files_info)
     }
   }
diff -r 11b2bf6f90d8 -r efc25bf4b795 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 05 21:29:25 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 05 22:49:25 2022 +0200
@@ -126,6 +126,9 @@
         case Nil => this
         case errs => error(cat_lines(errs))
       }
+
+    def base_info(session: String): Base_Info =
+      Base_Info(sessions_structure, errors, apply(session), Nil)
   }
 
   def deps(sessions_structure: Structure,