# HG changeset patch
# User wenzelm
# Date 1731251096 -3600
# Node ID 56bab51e02c1c2c690354337ff2882f4d35a00cf
# Parent  92fb366f708a57cebd38cad3d31276e971cb7fe5
performance tuning: more incremental update of buffer content;

diff -r 92fb366f708a -r 56bab51e02c1 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 15:11:04 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 16:04:56 2024 +0100
@@ -16,6 +16,7 @@
 
 import scala.util.parsing.input.CharSequenceReader
 import scala.jdk.CollectionConverters._
+import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
@@ -144,11 +145,32 @@
   def set_text(buffer: JEditBuffer, text: List[String]): Unit = {
     val old = buffer.isUndoInProgress
     def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
+
+    val length = buffer.getLength
+    var offset = 0
+
+    @tailrec def drop_common_prefix(list: List[String]): List[String] =
+      list match {
+        case s :: rest
+          if offset + s.length <= length &&
+          CharSequence.compare(buffer.getSegment(offset, s.length), s) == 0 =>
+            offset += s.length
+            drop_common_prefix(rest)
+        case _ => list
+      }
+
+    def insert(list: List[String]): Unit =
+      for (s <- list) {
+        buffer.insert(offset, s)
+        offset += s.length
+      }
+
     try {
       set(true)
       buffer.beginCompoundEdit()
-      buffer.remove(0, buffer.getLength)
-      buffer.insert(0, text.mkString)
+      val rest = drop_common_prefix(text)
+      if (offset < length) buffer.remove(offset, length - offset)
+      insert(rest)
     }
     finally {
       buffer.endCompoundEdit()