clarified output;
authorwenzelm
Wed, 06 Aug 2025 10:55:41 +0200
changeset 82953 d394a77ac023
parent 82952 430dcd883bbc
child 82954 1d6dc0eef4cf
clarified output;
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.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
     }
--- 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 */