more robust update;
authorwenzelm
Mon, 18 Nov 2024 14:47:17 +0100
changeset 81482 1001e27dbbf1
parent 81481 085393ed204a
child 81483 7d4df25af572
more robust update;
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()