src/Pure/Thy/text_edit.scala

--- a/src/Pure/Thy/text_edit.scala	Mon Jan 11 20:36:59 2010 +0100
+++ b/src/Pure/Thy/text_edit.scala	Mon Jan 11 20:50:03 2010 +0100
@@ -10,6 +10,10 @@
 
 class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
 {
+  override def toString =
+    (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
+
+
   /* transform offsets */
 
   private def transform(do_insert: Boolean, offset: Int): Int =