apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
--- 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()
}