# HG changeset patch
# User wenzelm
# Date 1483094794 -3600
# Node ID 7157685b71e302c8d68072b19e90866e136efb4d
# Parent  3ebf9f8299df3c15f53f9c0170457521eeb95939
clarified Document_Model perspective and edits;

diff -r 3ebf9f8299df -r 7157685b71e3 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 10:26:10 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 11:46:34 2016 +0100
@@ -12,9 +12,26 @@
 import scala.util.parsing.input.CharSequenceReader
 
 
-case class Document_Model(
-  session: Session, node_name: Document.Node.Name, doc: Line.Document,
-  changed: Boolean = true,
+object Document_Model
+{
+  def init(session: Session, node_name: Document.Node.Name, text: 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)))
+  }
+}
+
+sealed case class Document_Model private(
+  session: Session,
+  node_name: Document.Node.Name,
+  doc: Line.Document,
+  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,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
   /* name */
@@ -37,22 +54,39 @@
     }
 
 
+  /* perspective */
+
+  def text_perspective: Text.Perspective =
+    if (node_visible) Text.Perspective.full else Text.Perspective.empty
+
+  def node_perspective: Document.Node.Perspective_Text =
+    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
+
+
   /* edits */
 
-  def text_edits: List[Text.Edit] =
-    if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
+  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)
 
-  def node_edits: List[Document.Edit_Text] =
-    if (changed) {
-      List(session.header_edit(node_name, node_header),
-        node_name -> Document.Node.Clear(),
-        node_name -> Document.Node.Edits(text_edits),
-        node_name ->
-          Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
+      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))
     }
-    else Nil
-
-  def unchanged: Document_Model = if (changed) copy(changed = false) else this
+    else None
+  }
 
 
   /* diagnostics */
@@ -70,7 +104,7 @@
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
+  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
 }
diff -r 3ebf9f8299df -r 7157685b71e3 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 10:26:10 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:46:34 2016 +0100
@@ -114,7 +114,7 @@
 
   private def update_document(uri: String, text: String)
   {
-    val model = Document_Model(session, resources.node_name(uri), Line.Document(text, text_length))
+    val model = Document_Model.init(session, resources.node_name(uri), text)
     resources.update_model(model)
     delay_input.invoke()
   }
diff -r 3ebf9f8299df -r 7157685b71e3 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 10:26:10 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:46:34 2016 +0100
@@ -79,11 +79,12 @@
           (for {
             node_name <- st.pending_input.iterator
             model <- st.models.get(node_name.node)
-            if model.changed } yield model).toList
-        val edits = for { model <- changed; edit <- model.node_edits } yield edit
-        session.update(Document.Blobs.empty, edits)
+            res <- model.flush_edits
+          } yield res).toList
+
+        session.update(Document.Blobs.empty, changed.flatMap(_._1))
         st.copy(
-          models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+          models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
           pending_input = Set.empty)
       })
   }