# HG changeset patch
# User wenzelm
# Date 1672838790 -3600
# Node ID 2e791bdedec293f6af9b8c8eaa5ba6e5bf503fd5
# Parent  93ccf8b7a660c58ab23c727cc2b45b57d779670c
tuned;

diff -r 93ccf8b7a660 -r 2e791bdedec2 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Jan 04 13:39:40 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Jan 04 14:26:30 2023 +0100
@@ -513,8 +513,8 @@
               Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true)
             }
             blobs.get(name) match {
-              case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob)
-              case None => Some(name -> new_blob)
+              case Some(blob) if blob.bytes == bytes => None
+              case _ => Some(name -> new_blob)
             }
           }
         val blobs1 = new_blobs.foldLeft(blobs)(_ + _)