# HG changeset patch
# User wenzelm
# Date 1483116300 -3600
# Node ID 5e6566ab78bf48999fd58f5d06622fc0e4ad73db
# Parent  dd7f1a7e03f4b47b0a809161b339e56ea88ef739
more explicit edits -- eliminated Clear;

diff -r dd7f1a7e03f4 -r 5e6566ab78bf src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 11:54:11 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 17:45:00 2016 +0100
@@ -14,12 +14,12 @@
 
 object Document_Model
 {
-  def init(session: Session, node_name: Document.Node.Name, text: String): Document_Model =
+  def init(session: Session, uri: String): Document_Model =
   {
     val resources = session.resources.asInstanceOf[VSCode_Resources]
-    Document_Model(session, node_name, Line.Document(text, resources.text_length),
-      pending_clear = true,
-      pending_edits = List(Text.Edit.insert(0, text)))
+    val node_name = resources.node_name(uri)
+    val doc = Line.Document("", resources.text_length)
+    Document_Model(session, node_name, doc)
   }
 }
 
@@ -30,8 +30,7 @@
   node_visible: Boolean = true,
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
-  pending_clear: Boolean = false,
-  pending_edits: List[Text.Edit] = Nil,
+  pending_edits: Vector[Text.Edit] = Vector.empty,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
   /* name */
@@ -65,25 +64,31 @@
 
   /* edits */
 
+  def update_text(new_text: String): Document_Model =
+  {
+    val old_text = doc.make_text
+    if (new_text == old_text) this
+    else {
+      val doc1 = Line.Document(new_text, doc.text_length)
+      val pending_edits1 =
+        if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits
+      val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text)
+      copy(doc = doc1, pending_edits = pending_edits2)
+    }
+  }
+
   def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
   {
     val perspective = node_perspective
-    if (pending_clear || pending_edits.nonEmpty || last_perspective != perspective) {
-      val model1 = copy(pending_clear = false, pending_edits = Nil, last_perspective = perspective)
-
-      val header_edit = session.header_edit(node_name, node_header)
-      val edits: List[Document.Edit_Text] =
-        if (pending_clear)
-          List(header_edit,
-            node_name -> Document.Node.Clear(),
-            node_name -> Document.Node.Edits(pending_edits),
-            node_name -> perspective)
-        else
-          List(header_edit,
-            node_name -> Document.Node.Edits(pending_edits),
-            node_name -> perspective)
-
-      Some((edits.filterNot(_._2.is_void), model1))
+    if (pending_edits.nonEmpty || last_perspective != perspective) {
+      val text_edits = pending_edits.toList
+      val edits =
+        session.header_edit(node_name, node_header) ::
+        (if (text_edits.isEmpty) Nil
+         else List[Document.Edit_Text](node_name -> Document.Node.Edits(text_edits))) :::
+        (if (last_perspective == perspective) Nil
+         else List[Document.Edit_Text](node_name -> perspective))
+      Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective)))
     }
     else None
   }
@@ -104,7 +109,7 @@
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
+  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
 
   def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
 }
diff -r dd7f1a7e03f4 -r 5e6566ab78bf src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:54:11 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 17:45:00 2016 +0100
@@ -114,8 +114,7 @@
 
   private def update_document(uri: String, text: String)
   {
-    val model = Document_Model.init(session, resources.node_name(uri), text)
-    resources.update_model(model)
+    resources.update_model(session, uri, text)
     delay_input.invoke()
   }
 
diff -r dd7f1a7e03f4 -r 5e6566ab78bf src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:54:11 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 17:45:00 2016 +0100
@@ -60,12 +60,15 @@
 
   def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
 
-  def update_model(model: Document_Model)
+  def update_model(session: Session, uri: String, text: String)
   {
     state.change(st =>
-      st.copy(
-        models = st.models + (model.uri -> model),
-        pending_input = st.pending_input + model.uri))
+      {
+        val model = st.models.getOrElse(uri, Document_Model.init(session, uri)).update_text(text)
+        st.copy(
+          models = st.models + (uri -> model),
+          pending_input = st.pending_input + uri)
+      })
   }