src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Sat Jan 07 09:42:57 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Sat Jan 07 11:22:13 2017 +0100
@@ -139,6 +139,10 @@
   {
     def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
+    def replace(start: Offset, old_text: String, new_text: String): List[Edit] =
+      if (old_text == new_text) Nil
+      else if (old_text == "") List(insert(start, new_text))
+      else List(remove(start, old_text), insert(start, new_text))
   }
 
   final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)