clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 13:40:28 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 14:58:05 2024 +0100
@@ -92,12 +92,6 @@
 
   def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
 
-  def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = {
-    val undo_in_progress = buffer.isUndoInProgress
-    def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
-    try { set(true); body } finally { set(undo_in_progress) }
-  }
-
 
   /* main jEdit components */
 
@@ -141,12 +135,27 @@
   }
 
 
-  /* get text */
+  /* buffer text */
 
   def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
+  def set_text(buffer: JEditBuffer, text: List[String]): Unit = {
+    val old = buffer.isUndoInProgress
+    def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
+    try {
+      set(true)
+      buffer.beginCompoundEdit()
+      buffer.remove(0, buffer.getLength)
+      buffer.insert(0, text.mkString)
+    }
+    finally {
+      buffer.endCompoundEdit()
+      set(old)
+    }
+  }
+
 
   /* point range */
 

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 13:40:28 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 14:58:05 2024 +0100
@@ -120,7 +120,7 @@
               JEdit_Lib.buffer_edit(getBuffer) {
                 rich_text_area.active_reset()
                 getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
-                JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(rich_texts.map(_.text).mkString))
+                JEdit_Lib.set_text(getBuffer, rich_texts.map(_.text))
                 setCaretPosition(0)
               }
             }