# HG changeset patch # User wenzelm # Date 1732226826 -3600 # Node ID d421a7c58530e71c15bd143bd114d7fcaffdc1f0 # Parent da807cf1e461d4372693fd6961886737ed335f30 more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry); diff -r da807cf1e461 -r d421a7c58530 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 21 12:47:42 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 21 23:07:06 2024 +0100 @@ -23,26 +23,56 @@ import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler} import org.gjt.sp.jedit.textarea.JEditEmbeddedTextArea +import org.gjt.sp.jedit.search.HyperSearchResults import org.gjt.sp.jedit.syntax.SyntaxStyle import org.gjt.sp.jedit.gui.KeyEventTranslator -import org.gjt.sp.util.{SyntaxUtilities, Log} - +import org.gjt.sp.util.{SyntaxUtilities, Log, HtmlUtilities} object Pretty_Text_Area { + def make_highlight_style(): String = + HtmlUtilities.style2html(jEdit.getProperty(HyperSearchResults.HIGHLIGHT_PROP), + Font_Metric.default_font) + sealed case class Search_Result( buffer: JEditBuffer, + highlight_style: String, regex: Regex, line: Int, line_range: Text.Range ) { - lazy val match_ranges: List[Text.Range] = JEdit_Lib.search_text(buffer, line_range, regex) - lazy val line_text: String = JEdit_Lib.get_text(buffer, line_range).get - lazy val gui_text: String = line.toString + ": " + Library.trim_line(line_text) + lazy val line_text: String = + Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse("")) + + lazy val gui_text: String = { + // see also HyperSearchResults.highlightString + val s = new StringBuilder(line_range.length * 2) + s ++= "" + s ++= line.toString + s ++= ": " + + val line_start = line_range.start + val search_range = Text.Range(line_start, line_start + line_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) + s ++= "" + s ++= line_text.substring(next, next + range.length) + s ++= "" + last = range.stop - line_start + } + if (last < line_text.length) s ++= line_text.substring(last) + s ++= "" + s.toString + } override def toString: String = gui_text } sealed case class Search_Results( buffer: JEditBuffer, + highlight_style: String, pattern: Option[Regex] = None, results: List[Search_Result] = Nil ) { @@ -60,7 +90,7 @@ line <- (start_line until buffer.getLineCount).iterator line_range = JEdit_Lib.line_range(buffer, line) if JEdit_Lib.can_search_text(buffer, line_range, regex) - } yield Search_Result(buffer, regex, line, line_range)) + } yield Search_Result(buffer, highlight_style, regex, line, line_range)) (results1.length, copy(results = results1 ::: results2)) } @@ -98,7 +128,9 @@ new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action, get_search_pattern _, () => (), caret_visible = false, enable_hovering = true) - private var current_search_results = Pretty_Text_Area.Search_Results(getBuffer) + private var current_search_results = + Pretty_Text_Area.Search_Results(getBuffer, Pretty_Text_Area.make_highlight_style()) + def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_results.pattern } def handle_search(search: Pretty_Text_Area.Search_Results): Unit = ()