# HG changeset patch
# User wenzelm
# Date 1735314888 -3600
# Node ID c03e21a4cc2634e5c1e0c62280bea05c300593e2
# Parent  8a8814ab36f6798ef16e4e92ca545f9979e0328f
more accurate treatment of plain text (amending eede0cf38a63);

diff -r 8a8814ab36f6 -r c03e21a4cc26 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 27 16:14:16 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 27 16:54:48 2024 +0100
@@ -42,6 +42,7 @@
   ) {
     lazy val line_text: String =
       Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse(""))
+        .replace('\t',' ')
 
     lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s =>
       // see also HyperSearchResults.highlightString
@@ -50,20 +51,22 @@
       s ++= ":</b> "
 
       val line_start = line_range.start
-      val plain_text = line_text.replace('\t',' ').trim
-      val search_range = Text.Range(line_start, line_start + plain_text.length)
-      var last = 0
+      val plain_start = line_text.length - line_text.stripLeading.length
+      val plain_stop = line_text.stripTrailing.length
+
+      val search_range = Text.Range(line_start + plain_start, line_start + plain_stop)
+      var last = plain_start
       for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
         val next = range.start - line_start
-        if (last < next) s ++= plain_text.substring(last, next)
+        if (last < next) s ++= line_text.substring(last, next)
         s ++= "<span style=\""
         s ++= highlight_style
         s ++= "\">"
-        s ++= plain_text.substring(next, next + range.length)
+        s ++= line_text.substring(next, next + range.length)
         s ++= "</span>"
         last = range.stop - line_start
       }
-      if (last < plain_text.length) s ++= plain_text.substring(last)
+      if (last < plain_stop) s ++= line_text.substring(last)
       s ++= "</html>"
     }
     override def toString: String = gui_text