--- 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 ++= "<html><b>"
+ s ++= line.toString
+ s ++= ":</b> "
+
+ 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 ++= "<span style=\""
+ s ++= highlight_style
+ s ++= "\">"
+ s ++= line_text.substring(next, next + range.length)
+ s ++= "</span>"
+ last = range.stop - line_start
+ }
+ if (last < line_text.length) s ++= line_text.substring(last)
+ s ++= "</html>"
+ 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 = ()