# HG changeset patch
# User wenzelm
# Date 1674216534 -3600
# Node ID ac5ebdf198613b6b8e82310932e23cd231964bad
# Parent  40c6705603cbf38cdd45cc5d8a76e18713d88e80
clarified signature;

diff -r 40c6705603cb -r ac5ebdf19861 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Fri Jan 20 12:50:40 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Jan 20 13:08:54 2023 +0100
@@ -200,13 +200,10 @@
     session_background: Sessions.Background,
     progress: Log_Progress
   ): Unit = {
-    val store = JEdit_Sessions.sessions_store(PIDE.options.value)
     val document_selection = PIDE.editor.document_selection()
 
     val snapshot = PIDE.session.await_stable_snapshot()
-    val session_context =
-      Export.open_session_context(store, PIDE.resources.session_background,
-        document_snapshot = Some(snapshot))
+    val session_context = JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))
     try {
       val context =
         Document_Build.context(session_context,
diff -r 40c6705603cb -r ac5ebdf19861 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jan 20 12:50:40 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jan 20 13:08:54 2023 +0100
@@ -43,9 +43,20 @@
     Sessions.load_structure(session_options(options), dirs = dirs)
   }
 
-  def sessions_store(options: Options): Sessions.Store =
+
+  /* database store */
+
+  def sessions_store(options: Options = PIDE.options.value): Sessions.Store =
     Sessions.store(session_options(options))
 
+  def open_session_context(
+    store: Sessions.Store = sessions_store(),
+    session_background: Sessions.Background = PIDE.resources.session_background,
+    document_snapshot: Option[Document.Snapshot] = None
+  ): Export.Session_Context = {
+    Export.open_session_context(store, session_background, document_snapshot = document_snapshot)
+  }
+
 
   /* raw logic info */
 
@@ -148,7 +159,7 @@
   def session_start(options: Options): Unit = {
     val session = PIDE.session
     val session_background = PIDE.resources.session_background
-    val store = sessions_store(options)
+    val store = sessions_store(options = options)
 
     session.phase_changed += PIDE.plugin.session_phase_changed