# HG changeset patch
# User wenzelm
# Date 1659797641 -7200
# Node ID 5470c67bd772f8b965754a556de8913003cf2d9b
# Parent  d18c96b9b955aa1c06ff3b765e055583e2531246
clarified signature: prefer Export.Session_Context;

diff -r d18c96b9b955 -r 5470c67bd772 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 06 16:37:23 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 16:54:01 2022 +0200
@@ -248,6 +248,9 @@
   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,
@@ -271,6 +274,9 @@
 
     def close(): Unit = ()
 
+    def open_session0(session: String, close_context: Boolean = false): Session_Context =
+      open_session(Sessions.base_info0(session), close_context = close_context)
+
     def open_session(
       session_base_info: Sessions.Base_Info,
       document_snapshot: Option[Document.Snapshot] = None,
@@ -314,6 +320,8 @@
 
     def close(): Unit = ()
 
+    def db_context: Sessions.Database_Context = export_context.db_context
+
     def cache: Term.Cache = export_context.db_context.cache
 
     def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
diff -r d18c96b9b955 -r 5470c67bd772 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 06 16:37:23 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 06 16:54:01 2022 +0200
@@ -378,7 +378,7 @@
     def session: String = base.session_name
   }
 
-  def base_info_empty(session: String): Base_Info =
+  def base_info0(session: String): Base_Info =
     Base_Info(Base(session_name = session))
 
   def base_info(options: Options,
diff -r d18c96b9b955 -r 5470c67bd772 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Aug 06 16:37:23 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Aug 06 16:54:01 2022 +0200
@@ -13,19 +13,6 @@
 object Build_Job {
   /* theory markup/messages from session database */
 
-  def read_session_theory(
-    db_context: Sessions.Database_Context,
-    session: String,
-    theory: String,
-    unicode_symbols: Boolean = false
-  ): Option[Command] = {
-    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
@@ -102,9 +89,9 @@
     val store = Sessions.store(options)
     val session = new Session(options, Resources.empty)
 
-    using(store.open_database_context()) { db_context =>
+    using(Export.open_session_context0(store, session_name)) { session_context =>
       val result =
-        db_context.database(session_name) { db =>
+        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))
@@ -122,8 +109,7 @@
           for (thy <- print_theories) {
             val thy_heading = "\nTheory " + quote(thy) + ":"
 
-            read_session_theory(db_context, session_name, thy, unicode_symbols = unicode_symbols)
-            match {
+            read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
                 val snapshot = Document.State.init.snippet(command)
diff -r d18c96b9b955 -r 5470c67bd772 src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Sat Aug 06 16:37:23 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sat Aug 06 16:54:01 2022 +0200
@@ -17,8 +17,9 @@
   ): Unit = {
     val store = Sessions.store(options)
 
-    using(store.open_database_context()) { db_context =>
-      db_context.database(session)(db => Some(store.read_theories(db, session))) match {
+    using(Export.open_session_context0(store, session)) { session_context =>
+      session_context.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 {
@@ -29,7 +30,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              command <- Build_Job.read_session_theory(db_context, session, thy).iterator
+              command <- Build_Job.read_theory(session_context.theory(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