src/Tools/Graphview/popups.scala

--- a/src/Tools/Graphview/popups.scala	Wed Jan 07 18:09:11 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Thu Jan 08 20:56:39 2015 +0100
@@ -126,7 +126,7 @@
 
       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)