tuned;
authorwenzelm
Sat, 28 Jun 2025 15:55:35 +0200
changeset 82790 42a4d2ab2d54
parent 82789 941b6cdf3611
child 82791 57527794c788
tuned;
src/Pure/PIDE/document.scala
--- 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)