# HG changeset patch
# User wenzelm
# Date 1731937637 -3600
# Node ID 1001e27dbbf16709bcd147dbc29eb1c270ee292d
# Parent  085393ed204a9bee6779357207ba9d831cfe5246
more robust update;

diff -r 085393ed204a -r 1001e27dbbf1 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 14:35:48 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 14:47:17 2024 +0100
@@ -175,8 +175,9 @@
                 else 0)
               JEdit_Lib.scroll_to_caret(pretty_text_area)
 
-              val (unchanged_length, search_results) = current_search_results.update(update_start)
-              if (unchanged_length < search_results.length) {
+              val (search_update_start, search_results) =
+                current_search_results.update(update_start)
+              if (current_search_results != search_results) {
                 current_search_results = search_results
                 handle_search(search_results)
                 pretty_text_area.getPainter.repaint()