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