# HG changeset patch
# User wenzelm
# Date 1731164467 -3600
# Node ID 84cf218e052a912f1b920729d5f6bbd1d6d2d986
# Parent  07c802837a8cf04ee088c4049d8d4679134671c8
performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);

diff -r 07c802837a8c -r 84cf218e052a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:01:07 2024 +0100
@@ -90,19 +90,17 @@
       val metric = JEdit_Lib.font_metric(getPainter)
       val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.average_width).toInt)
 
+      val output = current_output
       val snapshot = current_base_snapshot
       val results = current_base_results
-      val formatted =
-        Pretty.formatted(Pretty.separate(current_output), margin = margin, metric = metric)
 
       future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
-          val (text, rendering) =
-            try {
-              val rich_text = Command.rich_text(body = formatted, results = results)
-              (rich_text.source, JEdit_Rendering(snapshot, rich_text))
-            }
+          val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
+          val rich_text = Command.rich_text(body = formatted, results = results)
+          val rendering =
+            try { JEdit_Rendering(snapshot, rich_text) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
           Exn.Interrupt.expose()
 
@@ -111,7 +109,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(text))
+              JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(rich_text.source))
               setCaretPosition(0)
             }
           }