# HG changeset patch
# User wenzelm
# Date 1659798979 -7200
# Node ID f49c4f160b8423e052dedcab3961ceb9845e172d
# Parent  5470c67bd772f8b965754a556de8913003cf2d9b
clarified signature: find session_database within Session_Context.db_hierarchy;

diff -r 5470c67bd772 -r f49c4f160b84 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 06 16:54:01 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 17:16:19 2022 +0200
@@ -332,6 +332,12 @@
       if (document_snapshot.isDefined) Sessions.DRAFT
       else session_base.session_name
 
+    def session_database(session: String = session_name): Option[Session_Database] =
+      db_hierarchy.find(_.session == session)
+
+    def session_db(session: String = session_name): Option[SQL.Database] =
+      session_database(session = session).map(_.db)
+
     def session_stack: List[String] =
       ((if (document_snapshot.isDefined) List(session_name) else Nil) :::
         db_hierarchy.map(_.session)).reverse
@@ -349,7 +355,7 @@
             res <- select1(entry_name).iterator
           } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
         }
-        else { db_hierarchy.find(_.session == name).map(select2).getOrElse(Nil) }
+        else { session_database(name).map(select2).getOrElse(Nil) }
       if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
     }
 
@@ -386,10 +392,6 @@
     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) + ")"
   }
diff -r 5470c67bd772 -r f49c4f160b84 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 06 16:54:01 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 06 17:16:19 2022 +0200
@@ -544,7 +544,8 @@
     val documents =
       for {
         doc <- info.document_variants
-        document <- session_context.read_document(session, doc.name)
+        db <- session_context.session_db()
+        document <- Document_Build.read_document(db, session, doc.name)
       } yield {
         val doc_path = (session_dir + doc.path.pdf).expand
         if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
diff -r 5470c67bd772 -r f49c4f160b84 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Aug 06 16:54:01 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Aug 06 17:16:19 2022 +0200
@@ -91,11 +91,12 @@
 
     using(Export.open_session_context0(store, session_name)) { session_context =>
       val result =
-        session_context.db_context.database(session_name) { db =>
-          val theories = store.read_theories(db, session_name)
-          val errors = store.read_errors(db, session_name)
-          store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
-        }
+        for {
+          db <- session_context.session_db()
+          theories = store.read_theories(db, session_name)
+          errors = store.read_errors(db, session_name)
+          info <- store.read_build(db, session_name)
+        } yield (theories, errors, info.return_code)
       result match {
         case None => error("Missing build database for session " + quote(session_name))
         case Some((used_theories, errors, rc)) =>
diff -r 5470c67bd772 -r f49c4f160b84 src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Sat Aug 06 16:54:01 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sat Aug 06 17:16:19 2022 +0200
@@ -18,8 +18,7 @@
     val store = Sessions.store(options)
 
     using(Export.open_session_context0(store, session)) { session_context =>
-      session_context.db_context.database(session)(db => Some(store.read_theories(db, session)))
-      match {
+      session_context.session_db().map(db => 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 {