# HG changeset patch
# User wenzelm
# Date 1731869365 -3600
# Node ID eaf5c460ceb585981bbd623ab03bc00c94d4dfc8
# Parent  a3dc66165d1546d97ccabd89a559d51ce93d25a0
more operations, to support search within output panel;

diff -r a3dc66165d15 -r eaf5c460ceb5 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 17 13:57:50 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 17 19:49:25 2024 +0100
@@ -144,6 +144,10 @@
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
+  def can_search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): Boolean =
+    try { regex.findFirstIn(buffer.getSegment(range.start, range.length)).nonEmpty }
+    catch { case _: ArrayIndexOutOfBoundsException => false }
+
   def search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): List[Text.Range] =
     List.from(
       for {
diff -r a3dc66165d15 -r eaf5c460ceb5 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Sun Nov 17 13:57:50 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Sun Nov 17 19:49:25 2024 +0100
@@ -14,12 +14,47 @@
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
 
+import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
+object Output_Area {
+  sealed case class Search_Result(
+    buffer: JEditBuffer,
+    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 = "<b>% 3d".format(line) + ":</b> " + Library.trim_line(line_text)
+    override def toString: String = gui_text
+  }
+
+  sealed case class Search_Results(
+    buffer: JEditBuffer,
+    regex: Regex,
+    results: List[Search_Result]
+  ) {
+    def update(start_offset: Int): (Int, Search_Results) = {
+      val start_line = buffer.getLineOfOffset(start_offset)
+      val results1 = results.takeWhile(result => result.line < start_line)
+      val results2 =
+        List.from(
+          for {
+            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))
+      (results1.length, copy(results = results1 ::: results2))
+    }
+  }
+}
+
 class Output_Area(view: View, root_name: String = "Overview") {
   GUI_Thread.require {}