# HG changeset patch
# User wenzelm
# Date 1730557370 -3600
# Node ID e3b0c7aec1ed567034a59ac66e3f24e1d0443864
# Parent  ccdbe1b538fcf9dda6a86b38d18a0f6042636e5b
clarified signature;

diff -r ccdbe1b538fc -r e3b0c7aec1ed src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 14:58:50 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:22:50 2024 +0100
@@ -90,6 +90,11 @@
         current_threads = new_threads
         current_output = new_output
       }
+
+      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
+        update_focus()
+        update_vals()
+      }
     }
 
   override def detach_operation: Option[() => Unit] =
@@ -103,14 +108,7 @@
   def tree: JTree = tree_text_area.tree
 
   def tree_selection(): Option[Debugger.Context] =
-    tree.getLastSelectedPathComponent match {
-      case node: DefaultMutableTreeNode =>
-        node.getUserObject match {
-          case c: Debugger.Context => Some(c)
-          case _ => None
-        }
-      case _ => None
-    }
+    tree_text_area.get_tree_selection({ case c: Debugger.Context => c })
 
   def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
@@ -163,10 +161,6 @@
     }
   }
 
-  tree.addTreeSelectionListener({ (_: TreeSelectionEvent) =>
-    update_focus()
-    update_vals()
-  })
   tree.addMouseListener(
     new MouseAdapter {
       override def mouseClicked(e: MouseEvent): Unit = {
diff -r ccdbe1b538fc -r e3b0c7aec1ed src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 14:58:50 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:22:50 2024 +0100
@@ -32,10 +32,18 @@
   /* tree view */
 
   val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
+  val tree: JTree = new JTree(root)
 
-  val tree: JTree = new JTree(root)
-  tree.setRowHeight(0)
-  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+  def get_tree_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
+    tree.getLastSelectedPathComponent match {
+      case node: DefaultMutableTreeNode =>
+        val obj = node.getUserObject
+        if (obj != null && which.isDefinedAt(obj)) Some(which(obj))
+        else None
+      case _ => None
+    }
+
+  def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
 
   def clear(): Unit = {
     tree.clearSelection()
@@ -45,6 +53,10 @@
   def reload(): Unit =
     tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
 
+  tree.setRowHeight(0)
+  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+  tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))
+
 
   /* text area */