# HG changeset patch
# User wenzelm
# Date 1420494069 -3600
# Node ID fef652c8826363f2c1d6af948cadccfff3e20809
# Parent  506660c6792fb20fdb2414f4106a75686fd00b06
proper bounding box including dummies;

diff -r 506660c6792f -r fef652c88263 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
 }
 
diff -r 506660c6792f -r fef652c88263 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 22:29:38 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 22:41:09 2015 +0100
@@ -55,7 +55,7 @@
 
   object Dummy
   {
-    def shape(visualizer: Visualizer, d: Layout.Point): Shape =
+    def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
     {
       val metrics = visualizer.metrics
       val w = metrics.space_width
diff -r 506660c6792f -r fef652c88263 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 22:29:38 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 22:41:09 2015 +0100
@@ -112,13 +112,14 @@
       var y0 = 0.0
       var x1 = 0.0
       var y1 = 0.0
-      for (node <- visible_graph.keys_iterator) {
-        val shape = Shapes.Node.shape(visualizer, node)
-        x0 = x0 min shape.getMinX
-        y0 = y0 min shape.getMinY
-        x1 = x1 max shape.getMaxX
-        y1 = y1 max shape.getMaxY
-      }
+      ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
+       (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
+         foreach(rect => {
+            x0 = x0 min rect.getMinX
+            y0 = y0 min rect.getMinY
+            x1 = x1 max rect.getMaxX
+            y1 = y1 max rect.getMaxY
+          })
       val gap = metrics.gap
       x0 = (x0 - gap).floor
       y0 = (y0 - gap).floor