src/Pure/PIDE/headless.scala
changeset 76902 2e791bdedec2
parent 76886 f405fcc3db33
child 76904 e27d097d7d15
--- 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)(_ + _)