--- 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 */