tuned;

--- a/src/Pure/PIDE/headless.scala	Wed Jan 04 14:56:22 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Jan 04 15:02:48 2023 +0100
@@ -508,13 +508,12 @@
         val new_blobs =
           names.flatMap { name =>
             val bytes = Bytes.read(name.path)
-            def new_blob: Document.Blobs.Item = {
-              val text = bytes.text
-              Document.Blobs.Item(bytes, text, Symbol.Text_Chunk(text), changed = true)
-            }
             blobs.get(name) match {
               case Some(blob) if blob.bytes == bytes => None
-              case _ => Some(name -> new_blob)
+              case _ =>
+                val text = bytes.text
+                val blob = Document.Blobs.Item(bytes, text, Symbol.Text_Chunk(text), changed = true)
+                Some(name -> blob)
             }
           }
         val blobs1 = new_blobs.foldLeft(blobs)(_ + _)