# HG changeset patch
# User wenzelm
# Date 1730903925 -3600
# Node ID 9421165bc1ac81308edd34e395396191de14da4d
# Parent  ae5695161423ddeb2c198c3bfbef206f6ed5f381
clarified modules;

diff -r ae5695161423 -r 9421165bc1ac src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 15:17:39 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 15:38:45 2024 +0100
@@ -68,11 +68,6 @@
 
   private val output: Output_Area =
     new Output_Area(view, root_name = "Threads") {
-      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
-        update_focus()
-        update_vals()
-      }
-
       override def handle_resize(): Unit = pretty_text_area.zoom(zoom)
 
       override def handle_update(): Unit = {
@@ -266,6 +261,11 @@
     JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
   }
 
+  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
+    update_focus()
+    update_vals()
+  })
+
 
   /* main */
 
diff -r ae5695161423 -r 9421165bc1ac src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Wed Nov 06 15:17:39 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Nov 06 15:38:45 2024 +0100
@@ -13,7 +13,6 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
-import javax.swing.event.TreeSelectionEvent
 
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
 import scala.swing.event.ButtonClicked
@@ -30,9 +29,6 @@
   val tree: Tree_View =
     new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
-  def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
-  tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))
-
 
   /* text area */