1.1 --- a/src/Pure/PIDE/text.scala	Sat Oct 22 23:29:11 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Oct 22 23:29:44 2011 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4      def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
     1.5    }
     1.6  
     1.7 -  class Edit(val is_insert: Boolean, val start: Offset, val text: String)
     1.8 +  class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
     1.9    {
    1.10      override def toString =
    1.11        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"