src/Tools/Graphview/layout.scala

--- a/src/Tools/Graphview/layout.scala	Mon Jan 05 22:29:38 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Jan 05 22:41:09 2015 +0100
@@ -310,5 +310,8 @@
         val dummies1 = dummies + (edge -> f(ds))
         new Layout(metrics, visible_graph, nodes, dummies1)
     }
+
+  def dummies_iterator: Iterator[Layout.Point] =
+    for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
 }