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