| changeset 59305 | b5e33012180e |
| parent 59304 | 848e27e4ac37 |
| child 59306 | cd2a0c14fe66 |
--- a/src/Tools/Graphview/layout.scala Tue Jan 06 16:43:17 2015 +0100 +++ b/src/Tools/Graphview/layout.scala Tue Jan 06 17:08:18 2015 +0100 @@ -332,9 +332,6 @@ /* dummies */ - def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] = - output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d }) - def dummies_iterator: Iterator[Layout.Point] = for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p