src/Tools/VSCode/src/vscode_resources.scala
changeset 66674 30d5195299e2
parent 66235 d4fa51e7c4ff
child 66676 39db5bb7eb0a
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 10:28:22 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 10:32:09 2017 +0200
@@ -155,13 +155,15 @@
     session: Session,
     editor: Server.Editor,
     file: JFile,
+    version: Long,
     text: String,
     range: Option[Line.Range] = None)
   {
     state.change(st =>
       {
         val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
-        val model1 = (model.change_text(text, range) getOrElse model).external(false)
+        val model1 =
+          (model.change_text(text, range) getOrElse model).set_version(version).external(false)
         st.update_models(Some(file -> model1))
       })
   }