# HG changeset patch
# User wenzelm
# Date 1750794583 -7200
# Node ID 0e36478a1b6a158c8cf7b31e85f8b9764acd8a57
# Parent  1629a57f3ef3c0a86fb152ffc80bd5b3624ae8fb
clarified signature: Session always provides Store (with Rich_Text.Cache);

diff -r 1629a57f3ef3 -r 0e36478a1b6a src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Jun 24 21:32:51 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Jun 24 21:49:43 2025 +0200
@@ -172,13 +172,12 @@
 
           val session =
             new Session(options) {
+              override val store: Store = store
+
               override val resources: Resources =
                 new Resources(session_background, log = log,
                   command_timings =
-                    Properties.uncompress(
-                      session_context.old_command_timings_blob, cache = store.cache))
-
-              override val cache: Rich_Text.Cache = store.cache
+                    Properties.uncompress(session_context.old_command_timings_blob, cache = cache))
 
               override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
                 Command.Blobs_Info.make(session_blobs(node_name))
diff -r 1629a57f3ef3 -r 0e36478a1b6a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Jun 24 21:32:51 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 24 21:49:43 2025 +0200
@@ -129,7 +129,8 @@
   val init_time: Time = Time.now()
   def print_now(): String = (Time.now() - init_time).toString
 
-  val cache: Rich_Text.Cache = Rich_Text.Cache.make()
+  val store: Store = Store(_session_options)
+  def cache: Rich_Text.Cache = store.cache
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty
   def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty
diff -r 1629a57f3ef3 -r 0e36478a1b6a src/Tools/jEdit/src/jedit_session.scala
--- a/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 21:32:51 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 21:49:43 2025 +0200
@@ -46,15 +46,12 @@
 
   /* database store */
 
-  def sessions_store(): Store =
-    Store(session_options(PIDE.options.value), cache = PIDE.session.cache)
-
   def open_session_context(
-    store: 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)
+    Export.open_session_context(
+      PIDE.session.store, session_background, document_snapshot = document_snapshot)
   }
 
 
@@ -164,19 +161,21 @@
     val options = PIDE.options.value
     val session = PIDE.session
     val session_background = PIDE.resources.session_background
-    val store = sessions_store()
     val session_heaps =
-      ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
+      ML_Process.session_heaps(session.store, session_background,
+        logic = session_background.session_name)
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
-    Isabelle_Process.start(store.options, session, session_background, session_heaps,
+    Isabelle_Process.start(session.store.options, session, session_background, session_heaps,
       modes =
-        (space_explode(',', store.options.string("jedit_print_mode")) :::
+        (space_explode(',', session.store.options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
   }
 }
 
 class JEdit_Session(_session_options: => Options) extends Session(_session_options) {
   override val resources: JEdit_Resources = JEdit_Resources(_session_options)
+
+  override val store: Store = Store(JEdit_Session.session_options(_session_options))
 }