clarified signature, with subtle change of semantics: proper non-null result;

--- a/src/Pure/GUI/tree_view.scala	Wed Nov 06 15:38:45 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Wed Nov 06 15:52:31 2024 +0100
@@ -20,7 +20,7 @@
 
     def unapply(tree_node: MutableTreeNode): Option[AnyRef] =
       tree_node match {
-        case node: Node => Some(node.getUserObject)
+        case node: Node if node.getUserObject != null => Some(node.getUserObject)
         case _ => None
       }
   }
@@ -32,7 +32,7 @@
 ) extends JTree(root) {
   def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
     getLastSelectedPathComponent match {
-      case Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj))
+      case Tree_View.Node(obj) if which.isDefinedAt(obj) => Some(which(obj))
       case _ => None
     }