--- 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 */
--- 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 _ =>