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