# HG changeset patch
# User wenzelm
# Date 1754479541 -7200
# Node ID 1d6dc0eef4cfcbf5553fc2bcc100c478483a7e60
# Parent  d394a77ac02331da08a57d6a2dc879ab9541ae3b
clarified output;

diff -r d394a77ac023 -r 1d6dc0eef4cf src/Pure/PIDE/document.scala
--- 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