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)