diff -r c7d2ae25d008 -r e891ff63e6db src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Jun 25 12:08:12 2025 +0200 +++ b/src/Pure/PIDE/session.scala Wed Jun 25 12:25:02 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 = store.cache + def cache: Rich_Text.Cache = if (store == null) Rich_Text.Cache.make() else 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