# HG changeset patch
# User wenzelm
# Date 1319318984 -7200
# Node ID feef63bcd7873f833207818a6c070754fb2c38c7
# Parent  b769a3a370ad7ae471052237490b075db31efbe4
class Text.Edit as abstract datatype;

diff -r b769a3a370ad -r feef63bcd787 src/Pure/PIDE/text.scala
--- 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 + ")"