# HG changeset patch
# User wenzelm
# Date 1659727082 -7200
# Node ID 9dbcc4c66e1c6b3bb7de3997d97558ee509b7a24
# Parent  26b71e1dd2627260630a0a83c2dd07cd808f120b
tuned signature: more operations;

diff -r 26b71e1dd262 -r 9dbcc4c66e1c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 21:10:41 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 21:18:02 2022 +0200
@@ -345,6 +345,16 @@
   def open_context(store: Sessions.Store): Context =
     new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
 
+  def open_session_context(
+    store: Sessions.Store,
+    session: String,
+    resources: Resources,
+    document_snapshot: Option[Document.Snapshot] = None
+  ): Session_Context = {
+    open_context(store)
+      .open_session(session, resources, document_snapshot = document_snapshot, close_context = true)
+  }
+
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
 
@@ -353,6 +363,8 @@
   }
 
   class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
+    context =>
+
     override def toString: String = db_context.toString
 
     def close(): Unit = ()
@@ -360,7 +372,8 @@
     def open_session(
       session: String,
       resources: Resources,
-      document_snapshot: Option[Document.Snapshot] = None
+      document_snapshot: Option[Document.Snapshot] = None,
+      close_context: Boolean = false
     ): Session_Context = {
       val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
       val session_databases: List[Session_Database] =
@@ -380,7 +393,10 @@
             }
         }
       new Session_Context(resources, db_context.cache, session_databases, document_snapshot) {
-        override def close(): Unit = session_databases.foreach(_.close())
+        override def close(): Unit = {
+          session_databases.foreach(_.close())
+          if (close_context) context.close()
+        }
       }
     }
   }