# HG changeset patch
# User wenzelm
# Date 1750797049 -7200
# Node ID c3c8e84f63c62a4546a24389dc93641366e478d0
# Parent  788d7f3caa414aa83bdd52a42446bb194292a33e
clarified signature: general Session.open_session_context;

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
diff -r 788d7f3caa41 -r c3c8e84f63c6 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jun 24 22:21:49 2025 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jun 24 22:30:49 2025 +0200
@@ -198,7 +198,7 @@
 
         val result = Exn.capture {
           val snapshot = document_session.get_snapshot
-          using(JEdit_Session.open_session_context(document_snapshot = Some(snapshot)))(
+          using(PIDE.session.open_session_context(document_snapshot = Some(snapshot)))(
             Document_Editor.build(_, document_session, progress))
         }
         val msgs =
diff -r 788d7f3caa41 -r c3c8e84f63c6 src/Tools/jEdit/src/jedit_session.scala
--- a/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 22:21:49 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 22:30:49 2025 +0200
@@ -44,17 +44,6 @@
   }
 
 
-  /* database store */
-
-  def open_session_context(
-    session_background: Sessions.Background = PIDE.resources.session_background,
-    document_snapshot: Option[Document.Snapshot] = None
-  ): Export.Session_Context = {
-    Export.open_session_context(
-      PIDE.session.store, session_background, document_snapshot = document_snapshot)
-  }
-
-
   /* raw logic info */
 
   private val jedit_logic_option = "jedit_logic"