# 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 }