--- 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 {
--- 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 {}