# HG changeset patch # User wenzelm # Date 1737024920 -3600 # Node ID 9755a8921fbc56e860df62ef39df36a69f054c1c # Parent 57b0a02e2774a345f881de88a8deee0cac5cc34d proper GUI.Style_HTML.make_text, e.g. for term "x < y"; diff -r 57b0a02e2774 -r 9755a8921fbc src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Jan 15 15:49:16 2025 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Jan 16 11:55:20 2025 +0100 @@ -45,6 +45,8 @@ .replace('\t',' ') lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s => + val style = GUI.Style_HTML + // see also HyperSearchResults.highlightString s ++= "" s ++= line.toString @@ -58,15 +60,15 @@ var last = plain_start 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 ++= style.make_text(line_text.substring(last, next)) s ++= "" - s ++= line_text.substring(next, next + range.length) + s ++= style.make_text(line_text.substring(next, next + range.length)) s ++= "" last = range.stop - line_start } - if (last < plain_stop) s ++= line_text.substring(last) + if (last < plain_stop) s ++= style.make_text(line_text.substring(last)) s ++= "" } override def toString: String = gui_text