--- a/src/Pure/PIDE/document.scala Wed Aug 06 10:55:41 2025 +0200
+++ b/src/Pure/PIDE/document.scala Wed Aug 06 13:25:41 2025 +0200
@@ -49,7 +49,10 @@
command_offset: Symbol.Offset = 0,
changed: Boolean = false
) {
- override def toString: String = "Blobs.Item(" + bytes.size + ")"
+ override def toString: String =
+ "Blobs.Item(bytes = " + bytes.size + ", source = " + source.length +
+ if_proper(command_offset > 0, ", command_offset = " + command_offset) +
+ if_proper(changed, ", changed = true") + ")"
def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
def unchanged: Item = if (changed) copy(changed = false) else this