# HG changeset patch
# User wenzelm
# Date 1734443773 -3600
# Node ID eede0cf38a63b96f7bafaf2bd4d2d8a7e0b5f574
# Parent  5c10597029954c03d9266cf15934d9fe0783ee45
tuned GUI: trim text as in org.gjt.sp.jedit.search.HyperSearchResult;

diff -r 5c1059702995 -r eede0cf38a63 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Dec 17 13:38:52 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Dec 17 14:56:13 2024 +0100
@@ -50,19 +50,20 @@
       s ++= ":</b> "
 
       val line_start = line_range.start
-      val search_range = Text.Range(line_start, line_start + line_text.length)
+      val plain_text = line_text.replace('\t',' ').trim
+      val search_range = Text.Range(line_start, line_start + plain_text.length)
       var last = 0
       for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
         val next = range.start - line_start
-        if (last < next) s ++= line_text.substring(last, next)
+        if (last < next) s ++= plain_text.substring(last, next)
         s ++= "<span style=\""
         s ++= highlight_style
         s ++= "\">"
-        s ++= line_text.substring(next, next + range.length)
+        s ++= plain_text.substring(next, next + range.length)
         s ++= "</span>"
         last = range.stop - line_start
       }
-      if (last < line_text.length) s ++= line_text.substring(last)
+      if (last < plain_text.length) s ++= plain_text.substring(last)
       s ++= "</html>"
     }
     override def toString: String = gui_text