author | wenzelm |
Sat, 28 Jun 2025 15:55:35 +0200 | |
changeset 82790 | 42a4d2ab2d54 |
parent 82789 | 941b6cdf3611 |
child 82791 | 57527794c788 |
--- a/src/Pure/PIDE/document.scala Sat Jun 28 15:45:55 2025 +0200 +++ b/src/Pure/PIDE/document.scala Sat Jun 28 15:55:35 2025 +0200 @@ -49,7 +49,7 @@ changed: Boolean ) { def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty - def unchanged: Item = copy(changed = false) + def unchanged: Item = if (changed) copy(changed = false) else this } def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs)