normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
--- 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)
--- 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()
}