# HG changeset patch
# User wenzelm
# Date 1505723529 -7200
# Node ID 30d5195299e259f9b64066da1f8fa62c49df22b0
# Parent  1e4450008c47339e12db563da8d80303b1853245
store document version;

diff -r 1e4450008c47 -r 30d5195299e2 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 10:28:22 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 10:32:09 2017 +0200
@@ -56,6 +56,7 @@
   editor: Server.Editor,
   node_name: Document.Node.Name,
   content: Document_Model.Content,
+  version: Option[Long] = None,
   external_file: Boolean = false,
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
@@ -66,10 +67,12 @@
   model =>
 
 
-  /* text */
+  /* content */
 
   def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
 
+  def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
+
 
   /* external file */
 
diff -r 1e4450008c47 -r 30d5195299e2 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 10:28:22 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 10:32:09 2017 +0200
@@ -153,7 +153,7 @@
     delay_output.invoke()
   }
 
-  private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
+  private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange])
   {
     val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange]
     @tailrec def norm(chs: List[Protocol.TextDocumentChange])
@@ -168,7 +168,7 @@
     }
     norm(changes)
     norm_changes.foreach(change =>
-      resources.change_model(session, editor, file, change.text, change.range))
+      resources.change_model(session, editor, file, version, change.text, change.range))
 
     delay_input.invoke()
     delay_output.invoke()
@@ -436,9 +436,10 @@
           case Protocol.Initialized(()) =>
           case Protocol.Shutdown(id) => shutdown(id)
           case Protocol.Exit(()) => exit()
-          case Protocol.DidOpenTextDocument(file, _, _, text) =>
-            change_document(file, List(Protocol.TextDocumentChange(None, text)))
-          case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
+          case Protocol.DidOpenTextDocument(file, _, version, text) =>
+            change_document(file, version, List(Protocol.TextDocumentChange(None, text)))
+          case Protocol.DidChangeTextDocument(file, version, changes) =>
+            change_document(file, version, changes)
           case Protocol.DidCloseTextDocument(file) => close_document(file)
           case Protocol.Completion(id, node_pos) => completion(id, node_pos)
           case Protocol.Include_Word(()) => update_dictionary(true, false)
diff -r 1e4450008c47 -r 30d5195299e2 src/Tools/VSCode/src/vscode_resources.scala
--- 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))
       })
   }