--- 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))
})
}