src/Pure/PIDE/session.scala

--- a/src/Pure/PIDE/session.scala	Tue Jun 24 22:21:49 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 24 22:30:49 2025 +0200
@@ -136,6 +136,16 @@
   def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty
 
 
+  /* session exports */
+
+  def open_session_context(
+    document_snapshot: Option[Document.Snapshot] = None
+  ): Export.Session_Context = {
+    Export.open_session_context(
+      store, resources.session_background, document_snapshot = document_snapshot)
+  }
+
+
   /* global flags */
 
   @volatile var timing: Boolean = false