# HG changeset patch
# User wenzelm
# Date 1731924413 -3600
# Node ID a774655375edbd82c4191cbc6b22b5f8bff45209
# Parent  c9256ac992147653e808445b075afe6aa6996ff7
clarified signature;

diff -r c9256ac99214 -r a774655375ed src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Sun Nov 17 20:14:57 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Mon Nov 18 11:06:53 2024 +0100
@@ -37,20 +37,23 @@
 
   sealed case class Search_Results(
     buffer: JEditBuffer,
-    regex: Regex,
+    pattern: Option[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))
+    def update(start_offset: Int): (Int, Search_Results) =
+    pattern match {
+      case None => (results.length, this)
+      case Some(regex) =>
+        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))
     }
   }
 }