# HG changeset patch
# User wenzelm
# Date 1731924771 -3600
# Node ID d9e8f594487e936c3b72b4ab29c1b7621884d844
# Parent  a774655375edbd82c4191cbc6b22b5f8bff45209
clarified modules;

diff -r a774655375ed -r d9e8f594487e src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Mon Nov 18 11:06:53 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Mon Nov 18 11:12:51 2024 +0100
@@ -19,45 +19,8 @@
 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,
-    pattern: Option[Regex],
-    results: List[Search_Result]
-  ) {
-    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))
-    }
-  }
-}
-
 class Output_Area(view: View, root_name: String = "Overview") {
   GUI_Thread.require {}
 
diff -r a774655375ed -r d9e8f594487e src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 11:06:53 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 11:12:51 2024 +0100
@@ -20,6 +20,7 @@
 import scala.util.matching.Regex
 
 import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
+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.syntax.SyntaxStyle
@@ -27,6 +28,42 @@
 import org.gjt.sp.util.{SyntaxUtilities, Log}
 
 
+object Pretty_Text_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,
+    pattern: Option[Regex],
+    results: List[Search_Result]
+  ) {
+    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))
+    }
+  }
+}
+
 class Pretty_Text_Area(
   view: View,
   close_action: () => Unit = () => (),