--- 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,
--- 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