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