tuned signature: more operations;

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 16 15:04:41 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 16 19:07:24 2024 +0100
@@ -16,6 +16,7 @@
 import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow, SwingUtilities}
 
 import scala.util.parsing.input.CharSequenceReader
+import scala.util.matching.Regex
 import scala.jdk.CollectionConverters._
 import scala.annotation.tailrec
 
@@ -143,6 +144,13 @@
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
+  def search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): List[Text.Range] =
+    List.from(
+      for {
+        s <- get_text(buffer, range).iterator
+        m <- regex.findAllMatchIn(s)
+      } yield Text.Range(range.start + m.start, range.start + m.end))
+
   def set_text(buffer: JEditBuffer, text: List[String]): Int = {
     val old = buffer.isUndoInProgress
     def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Nov 16 15:04:41 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Nov 16 19:07:24 2024 +0100
@@ -626,9 +626,7 @@
             // search pattern
             for {
               regex <- search_pattern
-              text <- JEdit_Lib.get_text(buffer, line_range)
-              m <- regex.findAllMatchIn(text)
-              range = Text.Range(m.start, m.end) + line_range.start
+              range <- JEdit_Lib.search_text(buffer, line_range, regex)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.search_color)