# HG changeset patch
# User wenzelm
# Date 1659867763 -7200
# Node ID ff6c1a82270fe3683dd5ba328ec1888c9b2a6551
# Parent  16135603d9c772663c21e2a43f42c6e5e9048599
clarified modules;

diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:22:43 2022 +0200
@@ -241,24 +241,7 @@
   }
 
 
-  /* context for retrieval */
-
-  def context(db_context: Sessions.Database_Context): Context = new Context(db_context)
-
-  def open_context(store: Sessions.Store): Context =
-    new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
-
-  def open_session_context0(store: Sessions.Store, session: String): Session_Context =
-    open_context(store).open_session0(session, close_context = true)
-
-  def open_session_context(
-    store: Sessions.Store,
-    session_base_info: Sessions.Base_Info,
-    document_snapshot: Option[Document.Snapshot] = None
-  ): Session_Context = {
-    open_context(store).open_session(
-      session_base_info, document_snapshot = document_snapshot, close_context = true)
-  }
+  /* context for database access */
 
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
@@ -267,31 +250,62 @@
     lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
   }
 
-  class Context private[Export](protected val db_context: Sessions.Database_Context)
-  extends AutoCloseable {
-    context =>
+  def open_database_context(store: Sessions.Store): Database_Context = {
+    val database_server = if (store.database_server) Some(store.open_database_server()) else None
+    new Database_Context(store, database_server)
+  }
+
+  def open_session_context0(store: Sessions.Store, session: String): Session_Context =
+    open_database_context(store).open_session0(session, close_database_context = true)
 
-    override def toString: String = db_context.toString
+  def open_session_context(
+    store: Sessions.Store,
+    session_base_info: Sessions.Base_Info,
+    document_snapshot: Option[Document.Snapshot] = None
+  ): Session_Context = {
+    open_database_context(store).open_session(
+      session_base_info, document_snapshot = document_snapshot, close_database_context = true)
+  }
 
-    def cache: Term.Cache = db_context.cache
+  class Database_Context private[Export](
+    val store: Sessions.Store,
+    val database_server: Option[SQL.Database]
+  ) extends AutoCloseable {
+    database_context =>
 
-    def close(): Unit = ()
+    override def toString: String = {
+      val s =
+        database_server match {
+          case Some(db) => db.toString
+          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
+        }
+      "Database_Context(" + s + ")"
+    }
+
+    def cache: Term.Cache = store.cache
 
-    def open_session0(session: String, close_context: Boolean = false): Session_Context =
-      open_session(Sessions.base_info0(session), close_context = close_context)
+    def close(): Unit = database_server.foreach(_.close())
+
+    def database_output[A](session: String)(f: SQL.Database => A): A =
+      database_server match {
+        case Some(db) => f(db)
+        case None => using(store.open_database(session, output = true))(f)
+      }
+
+    def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
+      open_session(Sessions.base_info0(session), close_database_context = close_database_context)
 
     def open_session(
       session_base_info: Sessions.Base_Info,
       document_snapshot: Option[Document.Snapshot] = None,
-      close_context: Boolean = false
+      close_database_context: Boolean = false
     ): Session_Context = {
       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 {
+        database_server match {
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
           case None =>
-            val store = db_context.store
             val attempts =
               session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
             attempts.collectFirst({ case (name, None) => name }) match {
@@ -304,17 +318,17 @@
                 }
             }
         }
-      new Session_Context(context, session_base_info, session_databases, document_snapshot) {
+      new Session_Context(database_context, session_base_info, session_databases, document_snapshot) {
         override def close(): Unit = {
           session_databases.foreach(_.close())
-          if (close_context) context.close()
+          if (close_database_context) database_context.close()
         }
       }
     }
   }
 
   class Session_Context private[Export](
-    val export_context: Context,
+    val database_context: Database_Context,
     session_base_info: Sessions.Base_Info,
     db_hierarchy: List[Session_Database],
     document_snapshot: Option[Document.Snapshot]
@@ -323,7 +337,7 @@
 
     def close(): Unit = ()
 
-    def cache: Term.Cache = export_context.cache
+    def cache: Term.Cache = database_context.cache
 
     def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
 
diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sun Aug 07 12:22:43 2022 +0200
@@ -113,13 +113,13 @@
     val empty: Nodes = new Nodes(Map.empty, Map.empty)
 
     def read(
-      export_context: Export.Context,
+      database_context: Export.Database_Context,
       deps: Sessions.Deps,
       presentation_sessions: List[String]
     ): Nodes = {
 
       def open_session(session: String): Export.Session_Context =
-        export_context.open_session(deps.base_info(session))
+        database_context.open_session(deps.base_info(session))
 
       type Batch = (String, List[String])
       val batches =
diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Aug 07 12:22:43 2022 +0200
@@ -1207,30 +1207,6 @@
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
 
-  class Database_Context private[Sessions](
-    val store: Sessions.Store,
-    val database_server: Option[SQL.Database]
-  ) extends AutoCloseable {
-    def cache: Term.Cache = store.cache
-
-    def close(): Unit = database_server.foreach(_.close())
-
-    def database_output[A](session: String)(f: SQL.Database => A): A =
-      database_server match {
-        case Some(db) => f(db)
-        case None => using(store.open_database(session, output = true))(f)
-      }
-
-    override def toString: String = {
-      val s =
-        database_server match {
-          case Some(db) => db.toString
-          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
-        }
-      "Database_Context(" + s + ")"
-    }
-  }
-
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
@@ -1310,9 +1286,6 @@
               port = options.int("build_database_ssh_port"))),
         ssh_close = true)
 
-    def open_database_context(server: Boolean = database_server): Database_Context =
-      new Database_Context(store, if (server) Some(open_database_server()) else None)
-
     def try_open_database(
       name: String,
       output: Boolean = false,
diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sun Aug 07 12:22:43 2022 +0200
@@ -494,9 +494,9 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        using(Export.open_context(store)) { export_context =>
+        using(Export.open_database_context(store)) { database_context =>
           val presentation_nodes =
-            Presentation.Nodes.read(export_context, deps, presentation_sessions.map(_.name))
+            Presentation.Nodes.read(database_context, deps, presentation_sessions.map(_.name))
 
           Par_List.map({ (session: String) =>
             progress.expose_interrupt()
@@ -510,7 +510,7 @@
                   deps.sessions_structure(deps(session).theory_qualifier(name))
               }
 
-            using(export_context.open_session(deps.base_info(session))) { session_context =>
+            using(database_context.open_session(deps.base_info(session))) { session_context =>
               Presentation.session_html(session_context, deps,
                 progress = progress,
                 verbose = verbose,
diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sun Aug 07 12:22:43 2022 +0200
@@ -441,16 +441,16 @@
       val (document_output, document_errors) =
         try {
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
-            using(store.open_database_context()) { db_context =>
+            using(Export.open_database_context(store)) { database_context =>
               val documents =
-                using(Export.context(db_context).open_session(deps.base_info(session_name))) {
+                using(database_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 =>
+              database_context.database_output(session_name)(db =>
                 documents.foreach(_.write(db, session_name)))
               (documents.flatMap(_.log_lines), Nil)
             }