src/Pure/Thy/export_theory.scala

     def theories: List[Theory] =
       theory_graph.topological_order.flatMap(theory)
   }
 
   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]]) {
         case (g, thy) => g.default_node(thy.name, Some(thy))
       }

           thy.parents.foldLeft(g0) {
             case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name)
           }
       }
 
-    Session(session_name, graph1)
+    Session(session_context.session_name, graph1)
   }
 
 
 
   /** theory content **/

         datatypes.map(_.cache(cache)),
         spec_rules.map(_.cache(cache)),
         (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 */
 
   object Kind {

         content.map(_.cache(cache)))
   }
   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]
   ): List[Entity[A]] = {
     def decode_entity(tree: XML.Tree): Entity[A] = {

           val content = if (body.isEmpty) None else Some(decode(body))
           Entity(kind, name, xname, pos, id, serial, content)
         case _ => err()
       }
     }
-    provider.uncompressed_yxml(export_name).map(decode_entity)
+    theory_context.uncompressed_yxml(export_name).map(decode_entity)
   }
 
 
   /* approximative syntax */
 

         syntax,
         args.map(cache.string),
         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) =
           triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
         Type(syntax, args, abbrev)

         cache.typ(typ),
         abbrev.map(cache.term),
         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)))) =
           pair(decode_syntax,
             pair(list(string),

 
   sealed case class Axiom(prop: Prop) extends Content[Axiom] {
     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,
     deps: List[String],
     proof: Term.Proof)

         prop.cache(cache),
         deps.map(cache.string),
         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._
         val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
         Thm(prop, deps, prf)

         cache.term(term),
         cache.proof(proof))
   }
 
   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))) = {
         import XML.Decode._
         import Term_XML.Decode._

       if (cache.no_cache) result else result.cache(cache)
     }
   }
 
   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
   ): List[(Thm_Id, Proof)] = {
     var seen = Set.empty[Long]

         case Term.AppP(p, q) => boxes(context, p); boxes(context, q)
         case thm: Term.PThm if !seen(thm.serial) =>
           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)
               case None =>
                 error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" +

       Class(
         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         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._
         val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body)
         Class(params, axioms)

         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
         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._
         val (typargs, args, axioms) =
           triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),

 
     def is_inclusion: Boolean =
       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._
         val (source, (target, (prefix, (subst_types, subst_terms)))) =
           pair(string, pair(string, pair(list(pair(string, bool)),
             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 */
 
   sealed case class Classrel(class1: String, class2: String, prop: Prop) {
     def cache(cache: Term.Cache): Classrel =
       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)
     }
     for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)

     def cache(cache: Term.Cache): Arity =
       Arity(cache.string(type_name), domain.map(cache.sort), cache.string(codomain),
         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._
       list(pair(decode_prop, triple(string, list(sort), string)))(body)
     }

   sealed case class Constdef(name: String, axiom_name: String) {
     def cache(cache: Term.Cache): Constdef =
       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)
     }
     for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name)

         cache.string(rep_name),
         cache.string(abs_name),
         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._
       list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
     }

         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         cache.typ(typ),
         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._
       list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)),
             pair(typ, list(pair(term, typ))))))))(body)

         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
         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._
       list(
         pair(properties, pair(string, pair(decode_rough_classification,

 
   sealed case class Other() extends Content[Other] {
     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
   }
 }