diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/text_edit.scala
--- a/src/Pure/PIDE/text_edit.scala	Mon Aug 16 12:11:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-/*  Title:      Pure/PIDE/text_edit.scala
-    Author:     Fabian Immler, TU Munich
-    Author:     Makarius
-
-Basic edits on plain text.
-*/
-
-package isabelle
-
-
-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 =
-    if (offset < start) offset
-    else if (is_insert == do_insert) offset + text.length
-    else (offset - text.length) max start
-
-  def convert(offset: Int): Int = transform(true, offset)
-  def revert(offset: Int): Int = transform(false, offset)
-
-
-  /* edit strings */
-
-  private def insert(index: Int, string: String): String =
-    string.substring(0, index) + text + string.substring(index)
-
-  private def remove(index: Int, count: Int, string: String): String =
-    string.substring(0, index) + string.substring(index + count)
-
-  def can_edit(string: String, shift: Int): Boolean =
-    shift <= start && start < shift + string.length
-
-  def edit(string: String, shift: Int): (Option[Text_Edit], String) =
-    if (!can_edit(string, shift)) (Some(this), string)
-    else if (is_insert) (None, insert(start - shift, string))
-    else {
-      val index = start - shift
-      val count = text.length min (string.length - index)
-      val rest =
-        if (count == text.length) None
-        else Some(new Text_Edit(false, start, text.substring(count)))
-      (rest, remove(index, count, string))
-    }
-}
-