| changeset 76914 | 1bc50ffad6d2 |
| parent 76912 | ca872f20cf5b |
| child 77149 | 3991a35cd740 |
--- a/src/Pure/PIDE/session.scala Thu Jan 05 17:00:22 2023 +0100 +++ b/src/Pure/PIDE/session.scala Thu Jan 05 17:14:29 2023 +0100 @@ -125,7 +125,7 @@ val cache: Term.Cache = Term.Cache.make() - def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none + 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