# HG changeset patch
# User wenzelm
# Date 1659796643 -7200
# Node ID d18c96b9b955aa1c06ff3b765e055583e2531246
# Parent  ed32b5554ed3a3c3d736852ffd33b3f75b163987
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;

diff -r ed32b5554ed3 -r d18c96b9b955 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 06 14:31:46 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 16:37:23 2022 +0200
@@ -193,21 +193,6 @@
   }
 
 
-  /* specific entries */
-
-  def read_document_id(read: String => Entry): Option[Long] =
-    read(DOCUMENT_ID).text match {
-      case Value.Long(id) => Some(id)
-      case _ => None
-    }
-
-  def read_files(read: String => Entry): Option[(String, List[String])] =
-    split_lines(read(FILES).text) match {
-      case thy_file :: blobs_files => Some((thy_file, blobs_files))
-      case Nil => None
-    }
-
-
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
@@ -291,9 +276,8 @@
       document_snapshot: Option[Document.Snapshot] = None,
       close_context: Boolean = false
     ): Session_Context = {
-      val session_base = session_base_info.check.base
-      val session_hierarchy =
-        session_base_info.sessions_structure.build_hierarchy(session_base.session_name)
+      val session_name = session_base_info.check.base.session_name
+      val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
       val session_databases =
         db_context.database_server match {
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
@@ -311,7 +295,7 @@
                 }
             }
         }
-      new Session_Context(db_context.cache, session_base, session_databases, document_snapshot) {
+      new Session_Context(context, session_base_info, session_databases, document_snapshot) {
         override def close(): Unit = {
           session_databases.foreach(_.close())
           if (close_context) context.close()
@@ -321,8 +305,8 @@
   }
 
   class Session_Context private[Export](
-    val cache: Term.Cache,
-    session_base: Sessions.Base,
+    val export_context: Context,
+    session_base_info: Sessions.Base_Info,
     db_hierarchy: List[Session_Database],
     document_snapshot: Option[Document.Snapshot]
   ) extends AutoCloseable {
@@ -330,6 +314,12 @@
 
     def close(): Unit = ()
 
+    def cache: Term.Cache = export_context.db_context.cache
+
+    def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
+
+    def session_base: Sessions.Base = session_base_info.base
+
     def session_name: String =
       if (document_snapshot.isDefined) Sessions.DRAFT
       else session_base.session_name
@@ -388,6 +378,10 @@
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)
 
+    def read_document(session: String, name: String): Option[Document_Build.Document_Output] =
+      db_hierarchy.find(_.session == session).flatMap(session_db =>
+        Document_Build.read_document(session_db.db, session_db.session, name))
+
     override def toString: String =
       "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }
@@ -396,6 +390,8 @@
     val session_context: Session_Context,
     val theory: String
   ) {
+    def cache: Term.Cache = session_context.cache
+
     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)
@@ -406,6 +402,18 @@
         case None => Nil
       }
 
+    def document_id(): Option[Long] =
+      apply(DOCUMENT_ID, permissive = true).text match {
+        case Value.Long(id) => Some(id)
+        case _ => None
+      }
+
+    def files(): Option[(String, List[String])] =
+      split_lines(apply(FILES, permissive = true).text) match {
+        case Nil => None
+        case thy_file :: blobs_files => Some((thy_file, blobs_files))
+      }
+
     override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
   }
 
diff -r ed32b5554ed3 -r d18c96b9b955 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 06 14:31:46 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 06 16:37:23 2022 +0200
@@ -146,11 +146,11 @@
           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 {
+              theory_context.files() match {
                 case None => Nil
-                case Some((thy, other)) =>
+                case Some((thy, blobs)) =>
                   val thy_file_info = File_Info(theory, is_theory = true)
-                  (thy -> thy_file_info) :: other.map(_ -> File_Info(theory))
+                  (thy -> thy_file_info) :: blobs.map(_ -> File_Info(theory))
               }
             }
           }).toMap
@@ -524,19 +524,18 @@
   }
 
   def session_html(
-    session: String,
+    session_context: Export.Session_Context,
     deps: Sessions.Deps,
-    db_context: Sessions.Database_Context,
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
     session_elements: Elements
   ): Unit = {
-    val info = deps.sessions_structure(session)
+    val session = session_context.session_name
+    val info = session_context.sessions_structure(session)
     val options = info.options
-    val base = deps(session)
+    val base = session_context.session_base
 
-    val session_hierarchy = deps.sessions_structure.build_hierarchy(session)
     val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
 
     Bytes.write(session_dir + session_graph_path,
@@ -545,8 +544,7 @@
     val documents =
       for {
         doc <- info.document_variants
-        document <- db_context.database(session)(db =>
-          Document_Build.read_document(db, session, doc.name))
+        document <- session_context.read_document(session, doc.name)
       } yield {
         val doc_path = (session_dir + doc.path.pdf).expand
         if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
@@ -595,7 +593,7 @@
     def present_theory(name: Document.Node.Name): Option[XML.Body] = {
       progress.expose_interrupt()
 
-      Build_Job.read_theory(db_context, session_hierarchy, name.theory).flatMap { command =>
+      Build_Job.read_theory(session_context.theory(name.theory)).flatMap { command =>
         if (verbose) progress.echo("Presenting theory " + name)
         val snapshot = Document.State.init.snippet(command)
 
diff -r ed32b5554ed3 -r d18c96b9b955 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Aug 06 14:31:46 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Aug 06 16:37:23 2022 +0200
@@ -494,7 +494,9 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        using(store.open_database_context()) { db_context =>
+        using(Export.open_context(store)) { export_context =>
+          val db_context = export_context.db_context
+
           val presentation_nodes =
             Presentation.Nodes.read(presentation_sessions.map(_.name), deps, db_context)
 
@@ -509,10 +511,15 @@
                 override def theory_session(name: Document.Node.Name): Sessions.Info =
                   deps.sessions_structure(deps(session).theory_qualifier(name))
               }
-            Presentation.session_html(
-              session, deps, db_context, progress = progress,
-              verbose = verbose, html_context = html_context,
-              Presentation.elements1)
+
+            val session_base_info = deps.base_info(session)
+            using(export_context.open_session(session_base_info)) { session_context =>
+              Presentation.session_html(session_context, deps,
+                progress = progress,
+                verbose = verbose,
+                html_context = html_context,
+                Presentation.elements1)
+            }
           }, presentation_sessions.map(_.name))
         }
       }
diff -r ed32b5554ed3 -r d18c96b9b955 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Aug 06 14:31:46 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Aug 06 16:37:23 2022 +0200
@@ -11,28 +11,38 @@
 
 
 object Build_Job {
-  /* theory markup/messages from database */
+  /* theory markup/messages from session database */
 
-  def read_theory(
+  def read_session_theory(
     db_context: Sessions.Database_Context,
-    session_hierarchy: List[String],
+    session: String,
     theory: String,
     unicode_symbols: Boolean = false
   ): Option[Command] = {
-    def read(name: String): Export.Entry =
-      db_context.get_export(session_hierarchy, theory, name)
+    val export_context = Export.context(db_context)
+    val session_base_info = Sessions.base_info_empty(session)
+    using(export_context.open_session(session_base_info)) { session_context =>
+      Build_Job.read_theory(session_context.theory(theory), unicode_symbols = unicode_symbols)
+    }
+  }
+
+  def read_theory(
+    theory_context: Export.Theory_Context,
+    unicode_symbols: Boolean = false
+  ): Option[Command] = {
+    def read(name: String): Export.Entry = theory_context(name, permissive = true)
 
     def read_xml(name: String): XML.Body =
       YXML.parse_body(
         Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
-        cache = db_context.cache)
+        cache = theory_context.cache)
 
     for {
-      id <- Export.read_document_id(read)
-      (thy_file, blobs_files) <- Export.read_files(read)
+      id <- theory_context.document_id()
+      (thy_file, blobs_files) <- theory_context.files()
     }
     yield {
-      val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
+      val node_name = Resources.file_node(Path.explode(thy_file), theory = theory_context.theory)
 
       val results =
         Command.Results.make(
@@ -108,9 +118,11 @@
           }
           val print_theories =
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
+
           for (thy <- print_theories) {
             val thy_heading = "\nTheory " + quote(thy) + ":"
-            read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols)
+
+            read_session_theory(db_context, session_name, thy, unicode_symbols = unicode_symbols)
             match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
diff -r ed32b5554ed3 -r d18c96b9b955 src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Sat Aug 06 14:31:46 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sat Aug 06 16:37:23 2022 +0200
@@ -18,8 +18,7 @@
     val store = Sessions.store(options)
 
     using(store.open_database_context()) { db_context =>
-      val result = db_context.database(session)(db => Some(store.read_theories(db, session)))
-      result match {
+      db_context.database(session)(db => Some(store.read_theories(db, session))) match {
         case None => error("Missing build database for session " + quote(session))
         case Some(used_theories) =>
           theories.filterNot(used_theories.toSet) match {
@@ -30,7 +29,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              command <- Build_Job.read_theory(db_context, List(session), thy).iterator
+              command <- Build_Job.read_session_theory(db_context, session, thy).iterator
               snapshot = Document.State.init.snippet(command)
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList