# HG changeset patch
# User wenzelm
# Date 1754470541 -7200
# Node ID d394a77ac02331da08a57d6a2dc879ab9541ae3b
# Parent  430dcd883bbc5002446ebe5df9b33b65a57f82d2
clarified output;

diff -r 430dcd883bbc -r d394a77ac023 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 05 23:31:30 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 06 10:55:41 2025 +0200
@@ -49,6 +49,8 @@
       command_offset: Symbol.Offset = 0,
       changed: Boolean = false
     ) {
+      override def toString: String = "Blobs.Item(" + bytes.size + ")"
+
       def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
       def unchanged: Item = if (changed) copy(changed = false) else this
     }
diff -r 430dcd883bbc -r d394a77ac023 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Aug 05 23:31:30 2025 +0200
+++ b/src/Pure/PIDE/text.scala	Wed Aug 06 10:55:41 2025 +0200
@@ -152,7 +152,7 @@
 
   final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) {
     override def toString: String =
-      (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
+      (if (is_insert) "Insert(" else "Remove(") + (start, text.length).toString + ")"
 
 
     /* transform offsets */