# 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() }