# HG changeset patch
# User wenzelm
# Date 1750950841 -7200
# Node ID 7cb5ef6da1f0c4bddaf2fccac5684b2e0cf47f51
# Parent  8f866fd6fae1702670f0d0ed7b09e99bdac100aa
proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);

diff -r 8f866fd6fae1 -r 7cb5ef6da1f0 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Wed Jun 25 16:35:25 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Thu Jun 26 17:14:01 2025 +0200
@@ -172,7 +172,7 @@
 
           val session =
             new Session(options) {
-              override val store: Store = store
+              override val store: Store = build_context.store
 
               override val resources: Resources =
                 new Resources(session_background, log = log,
diff -r 8f866fd6fae1 -r 7cb5ef6da1f0 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Jun 25 16:35:25 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Jun 26 17:14:01 2025 +0200
@@ -130,7 +130,7 @@
   def print_now(): String = (Time.now() - init_time).toString
 
   val store: Store = Store(_session_options)
-  def cache: Rich_Text.Cache = if (store == null) Rich_Text.Cache.make() else store.cache
+  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