diff -r 9089639ba348 -r 4d985afc0565 src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -38,8 +38,16 @@
   def pad_x: Double = char_width * 1.5
   def pad_y: Double = char_width
 
+  def dummy_width2: Double = (pad_x / 2).ceil
+
   def box_width2(node: Graph_Display.Node): Double =
     ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
+
+  def box_width2(vertex: Layout.Vertex): Double =
+    vertex match {
+      case Layout.Node(node) => box_width2(node)
+      case _: Layout.Dummy => dummy_width2
+    }
   def box_gap: Double = gap.ceil
   def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
 }