# HG changeset patch
# User wenzelm
# Date 1489005674 -3600
# Node ID 35fefc2493110f9f910cfd03eaad97aa5679739f
# Parent  25bccf5bf33e4bbd1ebac963d6155edb75e10eaf
suppress vacuous edits;

diff -r 25bccf5bf33e -r 35fefc249311 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Mar 08 20:30:05 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Mar 08 21:41:14 2017 +0100
@@ -141,10 +141,13 @@
   {
     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 inserts(start: Offset, text: String): List[Edit] =
+      if (text == "") Nil else List(insert(start, text))
+    def removes(start: Offset, text: String): List[Edit] =
+      if (text == "") Nil else List(remove(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))
+      else removes(start, old_text) ::: inserts(start, new_text)
   }
 
   final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)