# HG changeset patch
# User wenzelm
# Date 1420381403 -3600
# Node ID c8bd83f8dad9b6fa8180be7c3694199c1f8709d8
# Parent  399506ee38a56df2e6ce8df3d0a7dbe297cf9caf
tuned;

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)
diff -r 399506ee38a5 -r c8bd83f8dad9 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 04 14:05:24 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 04 15:23:23 2015 +0100
@@ -145,16 +145,8 @@
 
     def update_layout()
     {
-      val m = metrics()
-      val visible_graph = model.make_visible_graph()
-
-      val max_width =
-        visible_graph.keys_iterator.map(node => m.string_bounds(node.toString).getWidth).max
-      val box_distance = (max_width + m.pad + m.gap).ceil
-      def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
-
       // FIXME avoid expensive operation on GUI thread
-      layout = Layout.make(visible_graph, box_distance, box_height _)
+      layout = Layout.make(metrics(), model.make_visible_graph())
     }
 
     def bounding_box(): Rectangle2D.Double =