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