# HG changeset patch
# User wenzelm
# Date 1420495517 -3600
# Node ID 305e79989d48d3ae993f1afbdc96fec0c8e35259
# Parent  fef652c8826363f2c1d6af948cadccfff3e20809
tuned metrics;

diff -r fef652c88263 -r 305e79989d48 src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala	Mon Jan 05 22:41:09 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Mon Jan 05 23:05:17 2015 +0100
@@ -35,10 +35,11 @@
   def height: Double = mix.getHeight
   def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
   def gap: Double = mix.getWidth
-  def pad: Double = char_width
+  def pad_x: Double = char_width * 1.5
+  def pad_y: Double = char_width
 
   def box_width2(node: Graph_Display.Node): Double =
-    ((string_bounds(node.toString).getWidth + pad) / 2).ceil
+    ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
   def box_gap: Double = gap.ceil
   def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
 }
diff -r fef652c88263 -r 305e79989d48 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 22:41:09 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 23:05:17 2015 +0100
@@ -26,8 +26,8 @@
       val metrics = visualizer.metrics
       val p = visualizer.Coordinates.get_node(node)
       val bounds = metrics.string_bounds(node.toString)
-      val w = bounds.getWidth + metrics.pad
-      val h = bounds.getHeight + metrics.pad
+      val w = bounds.getWidth + metrics.pad_x
+      val h = bounds.getHeight + metrics.pad_y
       new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
     }
 
@@ -58,7 +58,7 @@
     def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
     {
       val metrics = visualizer.metrics
-      val w = metrics.space_width
+      val w = metrics.pad_x
       new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
     }