diff -r 399506ee38a5 -r c8bd83f8dad9 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sun Jan 04 14:05:24 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Sun Jan 04 15:23:23 2015 +0100
@@ -28,10 +28,19 @@
   val pendulum_iterations = 10
   val minimize_crossings_iterations = 40
 
-  def make(graph: Graph_Display.Graph, box_distance: Double, box_height: Int => Double): Layout =
+  def make(metrics: Visualizer.Metrics, graph: Graph_Display.Graph): Layout =
   {
     if (graph.is_empty) empty
     else {
+      def box_width(key: Key): Double =
+        (metrics.string_bounds(key.toString).getWidth + metrics.pad).ceil
+
+      val box_distance = (graph.keys_iterator.map(box_width(_)).max + metrics.gap).ceil
+
+      def box_height(level: Level): Double =
+        (metrics.char_width * 1.5 * (5 max level.length)).ceil
+
+
       val initial_levels = level_map(graph)
 
       val (dummy_graph, dummies, dummy_levels) =
@@ -54,7 +63,7 @@
           case ((coords1, y), level) =>
             ((((coords1, 0.0) /: level) {
               case ((coords2, x), key) => (coords2 + (key -> (x, y)), x + box_distance)
-            })._1, y + box_height(level.length))
+            })._1, y + box_height(level))
         })._1
 
       val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)