# HG changeset patch
# User wenzelm
# Date 1732007497 -3600
# Node ID ed5e75468db3e40597ddb98a6b0208525057543f
# Parent  6ca7c8f56396c436ee20caecec996fdab2d69564
clarified signature: prefer defaults for Output_Dockable (and its variants);

diff -r 6ca7c8f56396 -r ed5e75468db3 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Nov 19 10:11:17 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Nov 19 10:11:37 2024 +0100
@@ -64,10 +64,17 @@
   private var current_output: List[XML.Tree] = Nil
 
 
-  /* pretty text area */
+  /* output area */
 
   private val output: Output_Area =
     new Output_Area(view, root_name = "Threads") {
+      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {}
+
+      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
+        update_focus()
+        update_vals()
+      }
+
       override def handle_update(): Unit = {
         val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
         val (new_threads, new_output) = debugger.status(tree_selection())
@@ -253,11 +260,6 @@
     JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
   }
 
-  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
-    update_focus()
-    update_vals()
-  })
-
 
   /* main */
 
diff -r 6ca7c8f56396 -r ed5e75468db3 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 10:11:17 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 10:11:37 2024 +0100
@@ -13,6 +13,7 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
+import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -21,7 +22,7 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View, root_name: String = "Overview") {
+class Output_Area(view: View, root_name: String = "Search results") {
   output_area =>
 
   GUI_Thread.require {}
@@ -32,6 +33,17 @@
   val tree: Tree_View =
     new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
+  def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
+    tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
+    tree.revalidate()
+  }
+
+  def handle_tree_selection(e: TreeSelectionEvent): Unit =
+    for (result <- tree.get_selection({ case x: Pretty_Text_Area.Search_Result => x })) {
+      pretty_text_area.setCaretPosition(result.line_range.start)
+      JEdit_Lib.scroll_to_caret(pretty_text_area)
+    }
+
 
   /* text area */
 
@@ -41,7 +53,6 @@
         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 = ()
 
@@ -77,6 +88,11 @@
       }
     }
 
+  private lazy val tree_selection_listener =
+    new TreeSelectionListener {
+      def valueChanged(e: TreeSelectionEvent): Unit = handle_tree_selection(e)
+    }
+
 
   /* GUI components */
 
@@ -101,6 +117,7 @@
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
+    tree.addTreeSelectionListener(tree_selection_listener)
     parent match {
       case dockable: Dockable => dockable.set_content(if (split) split_pane else text_pane)
       case _ =>
diff -r 6ca7c8f56396 -r ed5e75468db3 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Nov 19 10:11:17 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Nov 19 10:11:37 2024 +0100
@@ -11,7 +11,6 @@
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
-import javax.swing.event.TreeSelectionEvent
 
 import org.gjt.sp.jedit.View
 
@@ -26,16 +25,10 @@
   private var current_output: List[XML.Elem] = Nil
 
 
-  /* pretty text area */
+  /* output area */
 
   private val output: Output_Area =
-    new Output_Area(view, root_name = "Search results") {
-      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
-        tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
-        tree.revalidate()
-      }
-      override def handle_update(): Unit = dockable.handle_update(true)
-    }
+    new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) }
 
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
@@ -65,19 +58,6 @@
     }
   }
 
-
-  /* tree view */
-
-  private def tree_selection(): Option[Pretty_Text_Area.Search_Result] =
-    output.tree.get_selection({ case x: Pretty_Text_Area.Search_Result => x })
-
-  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
-    for (result <- tree_selection()) {
-      output.pretty_text_area.setCaretPosition(result.line_range.start)
-      JEdit_Lib.scroll_to_caret(output.pretty_text_area)
-    }
-  })
-
   output.init_gui(dockable, split = true)