# HG changeset patch
# User wenzelm
# Date 1730975739 -3600
# Node ID 83012fe972820105fa215abfc9e0ce21d2999d3f
# Parent  cbfc76aace10bc580c5ebe947d201c30ced0808c
revert 1206400b9b48: proper Node.unapply for Node.apply(null);

diff -r cbfc76aace10 -r 83012fe97282 src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Wed Nov 06 22:04:05 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Thu Nov 07 11:35:39 2024 +0100
@@ -20,7 +20,7 @@
 
     def unapply(tree_node: MutableTreeNode): Option[AnyRef] =
       tree_node match {
-        case node: Node if node.getUserObject != null => Some(node.getUserObject)
+        case node: Node => 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 which.isDefinedAt(obj) => Some(which(obj))
+      case Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj))
       case _ => None
     }