tuned;
authorwenzelm
Wed, 04 Jan 2023 14:26:30 +0100
changeset 76902 2e791bdedec2
parent 76901 93ccf8b7a660
child 76903 f9de9c4b2156
tuned;
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)(_ + _)