# HG changeset patch
# User wenzelm
# Date 1483784533 -3600
# Node ID e306cab8edf943509cf9ec11565b949e1cd7ed53
# Parent  899c69bad0a9dd5eab6ef23e25bfc94a8af63380
tuned;

diff -r 899c69bad0a9 -r e306cab8edf9 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sat Jan 07 09:42:57 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Sat Jan 07 11:22:13 2017 +0100
@@ -139,6 +139,10 @@
   {
     def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
+    def replace(start: Offset, old_text: String, new_text: String): List[Edit] =
+      if (old_text == new_text) Nil
+      else if (old_text == "") List(insert(start, new_text))
+      else List(remove(start, old_text), insert(start, new_text))
   }
 
   final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
diff -r 899c69bad0a9 -r e306cab8edf9 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 09:42:57 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 11:22:13 2017 +0100
@@ -31,7 +31,7 @@
   external_file: Boolean = false,
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
-  pending_edits: Vector[Text.Edit] = Vector.empty,
+  pending_edits: List[Text.Edit] = Nil,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model
 {
   /* external file */
@@ -85,19 +85,16 @@
 
   /* edits */
 
-  def is_stable: Boolean = pending_edits.isEmpty
-
   def update_text(text: String): Option[Document_Model] =
   {
+    val old_text = doc.make_text
     val new_text = Line.normalize(text)
-    val old_text = doc.make_text
-    if (new_text == old_text) None
-    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)
-      Some(copy(doc = doc1, pending_edits = pending_edits2))
+    Text.Edit.replace(0, old_text, new_text) match {
+      case Nil => None
+      case edits =>
+        val doc1 = Line.Document(new_text, doc.text_length)
+        val pending_edits1 = pending_edits ::: edits
+        Some(copy(doc = doc1, pending_edits = pending_edits1))
     }
   }
 
@@ -109,13 +106,13 @@
         get_blob match {
           case None =>
             List(session.header_edit(node_name, node_header),
-              node_name -> Document.Node.Edits(pending_edits.toList),
+              node_name -> Document.Node.Edits(pending_edits),
               node_name -> perspective)
           case Some(blob) =>
             List(node_name -> Document.Node.Blob(blob),
-              node_name -> Document.Node.Edits(pending_edits.toList))
+              node_name -> Document.Node.Edits(pending_edits))
         }
-      Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective)))
+      Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
     }
     else None
   }
@@ -136,7 +133,8 @@
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
+  def is_stable: Boolean = pending_edits.isEmpty
+  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
 }