class Text.Edit as abstract datatype;

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