--- 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
--- 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 =
--- 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"