# HG changeset patch
# User wenzelm
# Date 1731929816 -3600
# Node ID dd657c4bc2696b2492ccdff39a64b0659d8a5731
# Parent  d9e8f594487e936c3b72b4ab29c1b7621884d844
Output_Dockable: show search results as tree view;

diff -r d9e8f594487e -r dd657c4bc269 NEWS
--- a/NEWS	Mon Nov 18 11:12:51 2024 +0100
+++ b/NEWS	Mon Nov 18 12:36:56 2024 +0100
@@ -139,6 +139,8 @@
   - Highlighting works via mouse hovering alone, without requiring
     C-modifier.
 
+  - Search results are shown as tree view.
+
 * An active highlight area in the input buffer or output panel may be
 turned into a text selection by using the ALT modifier.
 
diff -r d9e8f594487e -r dd657c4bc269 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Mon Nov 18 11:12:51 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Mon Nov 18 12:36:56 2024 +0100
@@ -22,6 +22,8 @@
 
 
 class Output_Area(view: View, root_name: String = "Overview") {
+  output_area =>
+
   GUI_Thread.require {}
 
 
@@ -33,8 +35,13 @@
 
   /* text area */
 
-  val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
+  val pretty_text_area: Pretty_Text_Area =
+    new Pretty_Text_Area(view) {
+      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit =
+        output_area.handle_search(search)
+    }
 
+  def handle_search(search: Pretty_Text_Area.Search_Results): Unit = ()
   def handle_resize(): Unit = pretty_text_area.zoom()
   def handle_update(): Unit = ()
 
diff -r d9e8f594487e -r dd657c4bc269 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 18 11:12:51 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 18 12:36:56 2024 +0100
@@ -28,7 +28,14 @@
   /* pretty text area */
 
   private val output: Output_Area =
-    new Output_Area(view) {
+    new Output_Area(view, root_name = "Search results") {
+      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
+        tree.clear()
+        for (result <- search.results) tree.root.add(Tree_View.Node(result))
+        tree.reload_model()
+        tree.expandRow(0)
+        tree.revalidate()
+      }
       override def handle_update(): Unit = dockable.handle_update(true)
     }
 
@@ -60,7 +67,7 @@
     }
   }
 
-  output.init_gui(dockable)
+  output.init_gui(dockable, split = true)
 
 
   /* controls */
diff -r d9e8f594487e -r dd657c4bc269 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 11:12:51 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 12:36:56 2024 +0100
@@ -37,18 +37,20 @@
   ) {
     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)
+    lazy val gui_text: String = "% 3d".format(line) + ": " + 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]
+    pattern: Option[Regex] = None,
+    results: List[Search_Result] = Nil
   ) {
+    val length: Int = results.length
+
     def update(start_offset: Int): (Int, Search_Results) =
     pattern match {
-      case None => (results.length, this)
+      case None => (length, this)
       case Some(regex) =>
         val start_line = buffer.getLineOfOffset(start_offset)
         val results1 = results.takeWhile(result => result.line < start_line)
@@ -61,6 +63,10 @@
             } yield Search_Result(buffer, regex, line, line_range))
         (results1.length, copy(results = results1 ::: results2))
     }
+
+    def update_pattern(new_pattern: Option[Regex]): Option[Search_Results] =
+      if (pattern == new_pattern) None
+      else Some(copy(pattern = new_pattern, results = Nil).update(0)._2)
   }
 }
 
@@ -92,8 +98,9 @@
     new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action,
       get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
 
-  private var current_search_pattern: Option[Regex] = None
-  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
+  private var current_search_results = Pretty_Text_Area.Search_Results(getBuffer)
+  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_results.pattern }
+  def handle_search(search: Pretty_Text_Area.Search_Results): Unit = ()
 
   def get_background(): Option[Color] = None
 
@@ -167,6 +174,13 @@
                 else if (scroll_start < update_start) scroll_start
                 else 0)
               JEdit_Lib.scroll_to_caret(pretty_text_area)
+
+              val (unchanged_length, search_results) = current_search_results.update(update_start)
+              if (unchanged_length < search_results.length) {
+                current_search_results = search_results
+                handle_search(search_results)
+                pretty_text_area.getPainter.repaint()
+              }
             }
           }
         })
@@ -232,13 +246,14 @@
           val re = Library.make_regex(s)
           (re, re.isDefined)
       }
-    if (current_search_pattern != pattern) {
-      current_search_pattern = pattern
-      pretty_text_area.getPainter.repaint()
-    }
     text_field.setForeground(
       if (ok) search_field_foreground
       else current_rendering.color(Rendering.Color.error))
+    for (search_results <- current_search_results.update_pattern(pattern)) {
+      current_search_results = search_results
+      handle_search(search_results)
+      refresh()
+    }
   }