src/Tools/Graphview/popups.scala

       popup.add(filter_context(List(node), true, "Hide", true).peer)
       popup.add(filter_context(List(node), false, "Show only", false).peer)
 
       popup.add(new JPopupMenu.Separator)
     }
-    if (!selected_nodes.isEmpty) {
+    if (selected_nodes.nonEmpty) {
       val text =
         if (selected_nodes.length > 1) "multiple"
         else quote(selected_nodes.head.toString)
 
       popup.add(new MenuItem("Selected: " + text) { enabled = false }.peer)