# HG changeset patch
# User wenzelm
# Date 1750682560 -7200
# Node ID 085e624a1303e0572165d7c6eba8ad375284eba1
# Parent  0c83a22d8556834363e7cfa0c360e0a83f5a33ce
clarified signature, following c3793899b880;

diff -r 0c83a22d8556 -r 085e624a1303 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/Build/build.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -77,7 +77,7 @@
     results: Map[String, Process_Result],
     other_rc: Int
   ) {
-    def cache: Term.Cache = store.cache
+    def cache: Rich_Text.Cache = store.cache
 
     def sessions_ok: List[String] =
       List.from(
@@ -127,7 +127,7 @@
 
     final def build_store(options: Options,
       build_cluster: Boolean = false,
-      cache: Term.Cache = Term.Cache.make()
+      cache: Rich_Text.Cache = Rich_Text.Cache.make()
     ): Store = {
       val build_options = engine.build_options(options, build_cluster = build_cluster)
       val store = Store(build_options, build_cluster = build_cluster, cache = cache)
@@ -182,7 +182,7 @@
     export_files: Boolean = false,
     augment_options: String => List[Options.Spec] = _ => Nil,
     session_setup: (String, Session) => Unit = (_, _) => (),
-    cache: Term.Cache = Term.Cache.make()
+    cache: Rich_Text.Cache = Rich_Text.Cache.make()
   ): Results = {
     val engine = Engine(engine_name(options))
     val store = engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache)
diff -r 0c83a22d8556 -r 085e624a1303 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -177,7 +177,7 @@
 
           val session =
             new Session(options, resources) {
-              override val cache: Term.Cache = store.cache
+              override val cache: Rich_Text.Cache = store.cache
 
               override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
                 Command.Blobs_Info.make(session_blobs(node_name))
diff -r 0c83a22d8556 -r 085e624a1303 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/Build/build_schedule.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -1490,7 +1490,7 @@
     numa_shuffling: Boolean = false,
     augment_options: String => List[Options.Spec] = _ => Nil,
     session_setup: (String, Session) => Unit = (_, _) => (),
-    cache: Term.Cache = Term.Cache.make()
+    cache: Rich_Text.Cache = Rich_Text.Cache.make()
   ): Schedule = {
     Build.build_process(options, build_cluster = true, remove_builds = true)
 
diff -r 0c83a22d8556 -r 085e624a1303 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/Build/store.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -14,7 +14,7 @@
   def apply(
     options: Options,
     build_cluster: Boolean = false,
-    cache: Term.Cache = Term.Cache.make()
+    cache: Rich_Text.Cache = Rich_Text.Cache.make()
   ): Store = new Store(options, build_cluster, cache)
 
 
@@ -277,7 +277,7 @@
 class Store private(
     val options: Options,
     val build_cluster: Boolean,
-    val cache: Term.Cache
+    val cache: Rich_Text.Cache
   ) {
   store =>
 
diff -r 0c83a22d8556 -r 085e624a1303 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -127,7 +127,7 @@
   val init_time: Time = Time.now()
   def print_now(): String = (Time.now() - init_time).toString
 
-  val cache: Term.Cache = Term.Cache.make()
+  val cache: Rich_Text.Cache = Rich_Text.Cache.make()
 
   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 0c83a22d8556 -r 085e624a1303 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Mon Jun 23 14:42:40 2025 +0200
@@ -87,12 +87,7 @@
   /* session */
 
   private var _session: Session = null
-  private def init_session(): Unit = {
-    _session =
-      new Session(options.value, resources) {
-        override val cache: Term.Cache = Rich_Text.Cache.make()
-      }
-  }
+  private def init_session(): Unit = { _session = new Session(options.value, resources) }
   def session: Session = _session