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