# HG changeset patch
# User wenzelm
# Date 1420315974 -3600
# Node ID fac57c5a066d226b96e35f7916c961441c3a7a8f
# Parent  b12d76aa29fb7eb2013702047e952c720280f3c3
tuned;

diff -r b12d76aa29fb -r fac57c5a066d src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 21:07:05 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 21:12:54 2015 +0100
@@ -145,19 +145,16 @@
 
     def update_layout()
     {
-      layout =
-        if (model.current_graph.is_empty) Layout.empty
-        else {
-          val m = metrics()
+      val m = metrics()
 
-          val max_width =
-            model.current_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
+      val max_width =
+        model.current_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
 
-          Layout.make(model.current_graph, box_distance, box_height _)
-        }
+      // FIXME avoid expensive operation on GUI thread
+      layout = Layout.make(model.current_graph, box_distance, box_height _)
     }
 
     def bounding_box(): Rectangle2D.Double =