# HG changeset patch
# User wenzelm
# Date 1731242428 -3600
# Node ID b6928aa389f77e761b179df75c91f79b43c951ad
# Parent  8c1680ac41600a14cab46d18bbcfdec10c452bdd
minor performance tuning: avoid concatenation of existing string material;

diff -r 8c1680ac4160 -r b6928aa389f7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 10 12:56:38 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 10 13:40:28 2024 +0100
@@ -395,9 +395,6 @@
       markups = Markups.init(Markup_Tree.from_XML(body)))
   }
 
-  def full_source(commands: Iterable[Command]): String =
-    commands.iterator.map(_.source).mkString
-
 
   /* edits and perspective */
 
diff -r 8c1680ac4160 -r b6928aa389f7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Nov 10 12:56:38 2024 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Nov 10 13:40:28 2024 +0100
@@ -649,8 +649,18 @@
       val nodes2 = blobs.foldLeft(nodes1) { case (ns, (a, b)) => ns + (a -> Node.init_blob(b)) }
       val version1 = Version.make(nodes2)
 
+      val text_edits: List[Text.Edit] = {
+        var offset = 0
+        val result = new mutable.ListBuffer[Text.Edit]
+        for (command <- commands) {
+          result += Text.Edit.insert(offset, command.source)
+          offset += command.source.length
+        }
+        result.toList
+      }
+
       val edits: List[Edit_Text] =
-        List(node_name -> Node.Edits(List(Text.Edit.insert(0, Command.full_source(commands))))) :::
+        List(node_name -> Node.Edits(text_edits)) :::
         blobs.map({ case (a, b) => a -> Node.Blob(b) })
 
       val assign_update: Assign_Update =