equal
deleted
inserted
replaced
330 } |
330 } |
331 |
331 |
332 |
332 |
333 /* dummies */ |
333 /* dummies */ |
334 |
334 |
335 def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] = |
|
336 output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d }) |
|
337 |
|
338 def dummies_iterator: Iterator[Layout.Point] = |
335 def dummies_iterator: Iterator[Layout.Point] = |
339 for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p |
336 for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p |
340 |
337 |
341 def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] = |
338 def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] = |
342 new Iterator[Layout.Point] { |
339 new Iterator[Layout.Point] { |