# HG changeset patch
# User wenzelm
# Date 1730558557 -3600
# Node ID 5f28bded8d7d75921b34a0b27af6a339ffddd9b3
# Parent  a00d4d50b8513d9806ba67b5f2a43525505b72c5
clarified signature;

diff -r a00d4d50b851 -r 5f28bded8d7d src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:35:43 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:42:37 2024 +0100
@@ -71,6 +71,11 @@
 
   private val tree_text_area: Tree_Text_Area =
     new Tree_Text_Area(view, root_name = "Threads") {
+      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
+        update_focus()
+        update_vals()
+      }
+
       override def handle_resize(): Unit =
         GUI_Thread.require { pretty_text_area.zoom(zoom) }
 
@@ -91,10 +96,7 @@
         current_output = new_output
       }
 
-      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
-        update_focus()
-        update_vals()
-      }
+      override def handle_focus(): Unit = update_focus()
     }
 
   override def detach_operation: Option[() => Unit] =
@@ -102,16 +104,17 @@
 
   set_content(tree_text_area.main_pane)
   addComponentListener(tree_text_area.component_resize)
+  addFocusListener(tree_text_area.component_focus)
 
 
   /* tree view */
 
-  def tree: JTree = tree_text_area.tree
+  private def tree: JTree = tree_text_area.tree
 
-  def tree_selection(): Option[Debugger.Context] =
+  private def tree_selection(): Option[Debugger.Context] =
     tree_text_area.get_tree_selection({ case c: Debugger.Context => c })
 
-  def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
+  private def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
   private def update_tree(threads: Debugger.Threads): Unit = {
     val thread_contexts =
@@ -270,10 +273,6 @@
 
   override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()
 
-  addFocusListener(new FocusAdapter {
-    override def focusGained(e: FocusEvent): Unit = update_focus()
-  })
-
   private def update_focus(): Unit = {
     for (c <- tree_selection()) {
       debugger.set_focus(c)
diff -r a00d4d50b851 -r 5f28bded8d7d src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:35:43 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:42:37 2024 +0100
@@ -77,6 +77,11 @@
 
   /* main pane */
 
+  def handle_focus(): Unit = ()
+
+  lazy val component_focus: FocusAdapter =
+    new FocusAdapter { override def focusGained(e: FocusEvent): Unit = handle_focus() }
+
   val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
   tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always