proper edits;
authorwenzelm
Sun, 12 Mar 2017 19:06:10 +0100
changeset 65203 314246c6eeaa
parent 65202 187277b77d50
child 65204 d23eded35a33
child 65206 ff8c3c29a924
proper edits;
src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sun Mar 12 18:50:02 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sun Mar 12 19:06:10 2017 +0100
@@ -185,7 +185,7 @@
           if (l1 == l2) {
             if (0 <= c1 && c1 <= c2 && c2 <= s1.length) {
               Some(
-                if (lines1.isEmpty) ("", prefix)
+                if (lines1.isEmpty) ("", prefix ::: Document.split(insert))
                 else {
                   val removed_text = s1.substring(c1, c2)
                   val changed_text = s1.substring(0, c1) + insert + s1.substring(c2)
@@ -199,7 +199,7 @@
             val (s2, rest2) = Document.chop(lines2)
             if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) {
               Some(
-                if (lines1.isEmpty) ("", prefix)
+                if (lines1.isEmpty) ("", prefix ::: Document.split(insert))
                 else {
                   val r1 = s1.substring(c1)
                   val r2 = s2.substring(0, c2)