tuned;
authorwenzelm
Thu, 09 Mar 2017 15:27:37 +0100
changeset 65162 df1052d0708d
parent 65161 6af056380d0b
child 65163 d596a070f039
tuned;
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)