# HG changeset patch
# User wenzelm
# Date 1489069657 -3600
# Node ID df1052d0708df0db9b5a3516d88abf313748e734
# Parent  6af056380d0bcdbd35277e1cc1589be27cc4f621
tuned;

diff -r 6af056380d0b -r df1052d0708d src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Mar 09 15:20:45 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Mar 09 15:27:37 2017 +0100
@@ -143,13 +143,6 @@
     delay_output.invoke()
   }
 
-  private def update_document(file: JFile, text: String)
-  {
-    resources.change_model(session, file, text)
-    delay_input.invoke()
-    delay_output.invoke()
-  }
-
   private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   {
     changes.foreach(change => resources.change_model(session, file, change.text, change.range))
@@ -360,7 +353,8 @@
           case Protocol.Initialize(id) => init(id)
           case Protocol.Shutdown(id) => shutdown(id)
           case Protocol.Exit(()) => exit()
-          case Protocol.DidOpenTextDocument(file, _, _, text) => update_document(file, text)
+          case Protocol.DidOpenTextDocument(file, _, _, text) =>
+            change_document(file, List(Protocol.TextDocumentChange(None, text)))
           case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
           case Protocol.DidCloseTextDocument(file) => close_document(file)
           case Protocol.Completion(id, node_pos) => completion(id, node_pos)