# HG changeset patch
# User wenzelm
# Date 1731166773 -3600
# Node ID 2d9b6e32632ddbba17a53aac0a1c46e000ac3c8b
# Parent  4794576828df2624dfac18b69dece4c4836a9300
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;

diff -r 4794576828df -r 2d9b6e32632d src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:34:14 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:39:33 2024 +0100
@@ -104,12 +104,18 @@
           Exn.Interrupt.expose()
 
           GUI_Thread.later {
-            current_rendering = rendering
-            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_text.source))
-              setCaretPosition(0)
+            if (metric == JEdit_Lib.font_metric(getPainter) &&
+              output == current_output &&
+              snapshot == current_base_snapshot &&
+              results == current_base_results
+            ) {
+              current_rendering = rendering
+              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_text.source))
+                setCaretPosition(0)
+              }
             }
           }
         })