diff -r 788d7f3caa41 -r c3c8e84f63c6 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