# HG changeset patch
# User wenzelm
# Date 1420320858 -3600
# Node ID a80d2ef0b745bd007bb4cd1589b5ccdcd582eeee
# Parent  db265648139ce9b4c10fb9c15f31d079f67d17da
tuned;

diff -r db265648139c -r a80d2ef0b745 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Sat Jan 03 22:04:31 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Sat Jan 03 22:34:18 2015 +0100
@@ -24,7 +24,7 @@
     val visualizer = panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
-    val curr = visualizer.model.current_graph
+    val current_graph = visualizer.model.current_graph
 
     def filter_context(
         nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
@@ -54,28 +54,27 @@
           })
 
         if (edges) {
-          val outs =
-            nodes.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
-              .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
-          val ins =
-            nodes.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
-              .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
+          def degree_nodes(succs: Boolean) =
+            (for {
+              from <- nodes.iterator
+              tos = if (succs) current_graph.imm_succs(from) else current_graph.imm_preds(from)
+              if tos.nonEmpty
+            } yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering)
+
+          val outs = degree_nodes(true)
+          val ins = degree_nodes(false)
 
           if (outs.nonEmpty || ins.nonEmpty) {
             contents += new Separator()
-
             contents +=
               new Menu("Edge") {
                 if (outs.nonEmpty) {
                   contents += new MenuItem("From ...") { enabled = false }
-
-                  outs.map(e => {
-                    val (from, tos) = e
+                  for ((from, tos) <- outs) {
                     contents +=
                       new Menu(quote(from.toString)) {
                         contents += new MenuItem("To ...") { enabled = false }
-
-                        tos.toList.sorted(Graph_Display.Node.Ordering).distinct.map(to => {
+                        for (to <- tos) {
                           contents +=
                             new MenuItem(
                               new Action(quote(to.toString)) {
@@ -83,21 +82,18 @@
                                   add_mutator(
                                     Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
                               })
-                        })
+                        }
                       }
-                  })
+                  }
                 }
                 if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() }
                 if (ins.nonEmpty) {
                   contents += new MenuItem("To ...") { enabled = false }
-
-                  ins.map(e => {
-                    val (to, froms) = e
+                  for ((to, froms) <- ins) {
                     contents +=
                       new Menu(quote(to.toString)) {
                         contents += new MenuItem("From ...") { enabled = false }
-
-                        froms.toList.sorted(Graph_Display.Node.Ordering).distinct.map(from => {
+                        for (from <- froms) {
                           contents +=
                             new MenuItem(
                               new Action(quote(from.toString)) {
@@ -105,9 +101,9 @@
                                   add_mutator(
                                     Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
                               })
-                        })
+                        }
                       }
-                  })
+                  }
                 }
               }
           }