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