src/Tools/Graphview/src/model.scala

--- a/src/Tools/Graphview/src/model.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/model.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -75,10 +75,10 @@
       Node_List(Nil, false, false, false)
     ))  
   
-  def visible_nodes(): Iterator[String] = current.keys
+  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
   
-  def visible_edges(): Iterator[(String, String)] =
-    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator
+  def visible_edges_iterator: Iterator[(String, String)] =
+    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
   
   def complete = graph
   def current: Model.Graph =
@@ -96,7 +96,7 @@
     _colors = 
       (Map.empty[String, Color] /: Colors()) ({
           case (colors, (enabled, color, mutator)) => {
-              (colors /: mutator.mutate(graph, graph).keys) ({
+              (colors /: mutator.mutate(graph, graph).keys_iterator) ({
                   case (colors, k) => colors + (k -> color)
                 })
             }