clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
discontinued obsolete operations;

--- a/src/Pure/Admin/build_doc.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -54,9 +54,11 @@
             progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
-            using(store.open_database_context()) { db_context =>
-              Document_Build.build_documents(Document_Build.context(session, deps, db_context),
-                output_pdf = Some(Path.explode("~~/doc")))
+            using(Export.open_session_context(store, deps.base_info(session))) {
+              session_context =>
+                Document_Build.build_documents(
+                  Document_Build.context(session_context),
+                  output_pdf = Some(Path.explode("~~/doc")))
             }
             None
           }

--- a/src/Pure/Thy/document_build.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -116,30 +116,23 @@
       map(name => texinputs + Path.basic(name))
 
   def context(
-    session: String,
-    deps: Sessions.Deps,
-    db_context: Sessions.Database_Context,
+    session_context: Export.Session_Context,
     progress: Progress = new Progress
-  ): Context = {
-    val structure = deps.sessions_structure
-    val info = structure(session)
-    val base = deps(session)
-    val hierarchy = deps.sessions_structure.build_hierarchy(session)
-    val classpath = db_context.get_classpath(structure, session)
-    new Context(info, base, hierarchy, db_context, classpath, progress)
-  }
+  ): Context = new Context(session_context, progress)
 
   final class Context private[Document_Build](
-    info: Sessions.Info,
-    base: Sessions.Base,
-    hierarchy: List[String],
-    db_context: Sessions.Database_Context,
-    val classpath: List[File.Content_Bytes],
+    val session_context: Export.Session_Context,
     val progress: Progress = new Progress
   ) {
     /* session info */
 
-    def session: String = info.name
+    def session: String = session_context.session_name
+
+    private val info = session_context.sessions_structure(session)
+    private val base = session_context.session_base
+
+    val classpath: List[File.Content_Bytes] = session_context.classpath()
+
     def options: Options = info.options
 
     def document_bibliography: Boolean = options.bool("document_bibliography")
@@ -159,9 +152,6 @@
         .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
     }
 
-    def get_export(theory: String, name: String): Export.Entry =
-      db_context.get_export(hierarchy, theory, name)
-
 
     /* document content */
 
@@ -176,7 +166,8 @@
       for (name <- document_theories)
       yield {
         val path = Path.basic(tex_name(name))
-        val content = YXML.parse_body(get_export(name.theory, Export.DOCUMENT_LATEX).text)
+        val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+        val content = YXML.parse_body(entry.text)
         File.Content(path, content)
       }
 
@@ -255,7 +246,8 @@
 
     def old_document(directory: Directory): Option[Document_Output] =
       for {
-        old_doc <- db_context.database(session)(read_document(_, session, directory.doc.name))
+        db <- session_context.session_db()
+        old_doc <- read_document(db, session, directory.doc.name)
         if old_doc.sources == directory.sources
       }
       yield old_doc
@@ -481,12 +473,15 @@
             Sessions.load_structure(options + "document=pdf", dirs = dirs).
               selection_deps(Sessions.Selection.session(session))
 
+          val session_base_info = deps.base_info(session)
+
           if (output_sources.isEmpty && output_pdf.isEmpty) {
             progress.echo_warning("No output directory")
           }
 
-          using(store.open_database_context()) { db_context =>
-            build_documents(context(session, deps, db_context, progress = progress),
+          using(Export.open_session_context(store, session_base_info)) { session_context =>
+            build_documents(
+              context(session_context, progress = progress),
               output_sources = output_sources, output_pdf = output_pdf,
               verbose = verbose_latex)
           }

--- a/src/Pure/Thy/export.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -267,11 +267,14 @@
     lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
   }
 
-  class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
+  class Context private[Export](protected val db_context: Sessions.Database_Context)
+  extends AutoCloseable {
     context =>
 
     override def toString: String = db_context.toString
 
+    def cache: Term.Cache = db_context.cache
+
     def close(): Unit = ()
 
     def open_session0(session: String, close_context: Boolean = false): Session_Context =
@@ -320,9 +323,7 @@
 
     def close(): Unit = ()
 
-    def db_context: Sessions.Database_Context = export_context.db_context
-
-    def cache: Term.Cache = export_context.db_context.cache
+    def cache: Term.Cache = export_context.cache
 
     def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
 
@@ -392,7 +393,19 @@
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)
 
-    override def toString: String =
+    def classpath(): List[File.Content_Bytes] = {
+      (for {
+        session <- session_stack.iterator
+        info <- sessions_structure.get(session).iterator
+        if info.export_classpath.nonEmpty
+        matcher = make_matcher(info.export_classpath)
+        entry_name <- entry_names(session = session).iterator
+        if matcher(entry_name)
+        entry <- get(entry_name.theory, entry_name.name).iterator
+      } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList
+  }
+
+  override def toString: String =
       "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }
 

--- a/src/Pure/Thy/sessions.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -1221,56 +1221,6 @@
         case None => using(store.open_database(session, output = true))(f)
       }
 
-    def database[A](session: String)(f: SQL.Database => Option[A]): Option[A] =
-      database_server match {
-        case Some(db) => f(db)
-        case None =>
-          store.try_open_database(session) match {
-            case Some(db) => using(db)(f)
-            case None => None
-          }
-      }
-
-    def read_export(
-      session_hierarchy: List[String], theory: String, name: String
-    ): Option[Export.Entry] = {
-      def read(db: SQL.Database, session: String): Option[Export.Entry] =
-        Export.Entry_Name(session = session, theory = theory, name = name).read(db, store.cache)
-      val attempts =
-        database_server match {
-          case Some(db) => session_hierarchy.view.map(read(db, _))
-          case None =>
-            session_hierarchy.view.map(session =>
-              store.try_open_database(session) match {
-                case Some(db) => using(db) { _ => read(db, session) }
-                case None => None
-              })
-        }
-      attempts.collectFirst({ case Some(entry) => entry })
-    }
-
-    def get_export(session_hierarchy: List[String], theory: String, name: String): Export.Entry =
-      read_export(session_hierarchy, theory, name) getOrElse
-        Export.empty_entry(theory, name)
-
-    def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] =
-    {
-      (for {
-        name <- structure.build_requirements(List(session))
-        patterns = structure(name).export_classpath if patterns.nonEmpty
-      } yield {
-        database(name) { db =>
-          val matcher = Export.make_matcher(patterns)
-          val res =
-            for {
-              entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
-              entry <- entry_name.read(db, store.cache)
-            } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
-          Some(res)
-        }.getOrElse(Nil)
-      }).flatten
-    }
-
     override def toString: String = {
       val s =
         database_server match {

--- a/src/Pure/Tools/build_job.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -443,10 +443,13 @@
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
             using(store.open_database_context()) { db_context =>
               val documents =
-                Document_Build.build_documents(
-                  Document_Build.context(session_name, deps, db_context, progress = progress),
-                  output_sources = info.document_output,
-                  output_pdf = info.document_output)
+                using(Export.context(db_context).open_session(deps.base_info(session_name))) {
+                  session_context =>
+                    Document_Build.build_documents(
+                      Document_Build.context(session_context, progress = progress),
+                      output_sources = info.document_output,
+                      output_pdf = info.document_output)
+                }
               db_context.database_output(session_name)(db =>
                 documents.foreach(_.write(db, session_name)))
               (documents.flatMap(_.log_lines), Nil)