# HG changeset patch
# User wenzelm
# Date 1263239403 -3600
# Node ID c47a2228feadc63bd169227b236341373168cfa1
# Parent  f799f374959664e608074c647e190c712b3f12ac
Text_Edit.toString;

diff -r f799f3749596 -r c47a2228fead 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 =