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