# HG changeset patch
# User wenzelm
# Date 1730559806 -3600
# Node ID b796e59ec3efb8373173bb03d1ed249dc75ec926
# Parent  fad1278d0f5b8ece2e1bab53a9b5959fe8f44413
clarified modules;

diff -r fad1278d0f5b -r b796e59ec3ef src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:59:58 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 16:03:26 2024 +0100
@@ -163,14 +163,6 @@
     }
   }
 
-  tree.addMouseListener(
-    new MouseAdapter {
-      override def mouseClicked(e: MouseEvent): Unit = {
-        val click = tree.getPathForLocation(e.getX, e.getY)
-        if (click != null && e.getClickCount == 1) update_focus()
-      }
-    })
-
 
   /* controls */
 
diff -r fad1278d0f5b -r b796e59ec3ef src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:59:58 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:03:26 2024 +0100
@@ -98,6 +98,14 @@
         override def focusGained(e: FocusEvent): Unit = handle_focus()
       })
 
+    tree.addMouseListener(
+      new MouseAdapter {
+        override def mouseClicked(e: MouseEvent): Unit = {
+          val click = tree.getPathForLocation(e.getX, e.getY)
+          if (click != null && e.getClickCount == 1) handle_focus()
+        }
+      })
+
     component match {
       case dockable: Dockable => dockable.set_content(main_pane)
       case _ =>