--- 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) {