# HG changeset patch
# User wenzelm
# Date 1489238726 -3600
# Node ID 0f555ce33970604896969170c240a31cb5405856
# Parent  37f1effd6683c6ea49885b763db1a3256b0ffa63
apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);

diff -r 37f1effd6683 -r 0f555ce33970 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Mar 11 14:18:21 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Mar 11 14:25:26 2017 +0100
@@ -145,7 +145,8 @@
 
   private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   {
-    changes.foreach(change => resources.change_model(session, file, change.text, change.range))
+    changes.reverse.foreach(change =>
+      resources.change_model(session, file, change.text, change.range))
     delay_input.invoke()
     delay_output.invoke()
   }