# HG changeset patch
# User wenzelm
# Date 1489511301 -3600
# Node ID 1d6e9048cb6256d70407711d81c9389baf2bb9bc
# Parent  e37209c0a42a628aeb9b7b34927efeb6b30c2a72
normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;

diff -r e37209c0a42a -r 1d6e9048cb62 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Tue Mar 14 17:32:19 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Tue Mar 14 18:08:21 2017 +0100
@@ -26,6 +26,11 @@
   object Position
   {
     val zero: Position = Position()
+
+    object Ordering extends scala.math.Ordering[Position]
+    {
+      def compare(p1: Position, p2: Position): Int = p1 compare p2
+    }
   }
 
   sealed case class Position(line: Int = 0, column: Int = 0)
diff -r e37209c0a42a -r 1d6e9048cb62 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Mar 14 17:32:19 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Mar 14 18:08:21 2017 +0100
@@ -16,6 +16,7 @@
 import java.io.{PrintStream, OutputStream, File => JFile}
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 
 object Server
@@ -138,8 +139,21 @@
 
   private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   {
-    changes.reverse.foreach(change =>
+    val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange]
+    @tailrec def norm(chs: List[Protocol.TextDocumentChange])
+    {
+      if (chs.nonEmpty) {
+        val (full_texts, rest1) = chs.span(_.range.isEmpty)
+        val (edits, rest2) = rest1.span(_.range.nonEmpty)
+        norm_changes ++= full_texts
+        norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse
+        norm(rest2)
+      }
+    }
+    norm(changes)
+    norm_changes.foreach(change =>
       resources.change_model(session, file, change.text, change.range))
+
     delay_input.invoke()
     delay_output.invoke()
   }