# HG changeset patch
# User wenzelm
# Date 1734519578 -3600
# Node ID f57732142e0d4338548e962040f719c0253cfaab
# Parent  2cb49d09f0593188cf3eb27c2230f0bda640b04a
tuned GUI: more informative search_title;

diff -r 2cb49d09f059 -r f57732142e0d src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Dec 17 23:07:13 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Dec 18 11:59:38 2024 +0100
@@ -23,7 +23,7 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View, root_name: String = "Search results") {
+class Output_Area(view: View, root_name: String = Pretty_Text_Area.search_title()) {
   output_area =>
 
   GUI_Thread.require {}
@@ -43,7 +43,10 @@
       search_activated = true
       delay_shown.invoke()
     }
-    tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
+    tree.init_model {
+      tree.root.setUserObject(Pretty_Text_Area.search_title(lines = search.length))
+      for (result <- search.results) tree.root.add(Tree_View.Node(result))
+    }
     tree.revalidate()
   }
 
diff -r 2cb49d09f059 -r f57732142e0d src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Dec 17 23:07:13 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Dec 18 11:59:38 2024 +0100
@@ -69,6 +69,9 @@
     override def toString: String = gui_text
   }
 
+  def search_title(lines: Int = 0): String =
+    "Search result" + (if (lines <= 1) "" else " (" + lines + " lines)")
+
   sealed case class Search_Results(
     buffer: JEditBuffer,
     highlight_style: String,