diff -r dfa100466d2e -r dd6fc7c9504a src/Tools/Graphview/src/popups.scala
--- a/src/Tools/Graphview/src/popups.scala	Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/popups.scala	Mon Oct 08 23:29:07 2012 +0200
@@ -61,9 +61,9 @@
 
 
         if (edges) {
-          val outs = ls.map(l => (l, curr.imm_succs(l)))
+          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
                       .filter(_._2.size > 0).sortBy(_._1)
-          val ins = ls.map(l => (l, curr.imm_preds(l)))
+          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
                       .filter(_._2.size > 0).sortBy(_._1)
 
           if (outs.nonEmpty || ins.nonEmpty) {