# HG changeset patch
# User wenzelm
# Date 1421580985 -3600
# Node ID 04cdfd536e7d8120fa51ef8c98ec29a03ef7362d
# Parent  d15a96149703f0e71d814042f034bccaa63e6b22
tuned metrics;

diff -r d15a96149703 -r 04cdfd536e7d src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala	Sat Jan 17 23:33:21 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Sun Jan 18 12:36:25 2015 +0100
@@ -35,18 +35,16 @@
   def char_width: Double = mix.getWidth / 3
   def height: Double = mix.getHeight
   def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
-  def pad_x: Double = char_width * 1.5
-  def pad_y: Double = char_width
 
   def gap: Double = mix.getWidth.ceil
 
-  def dummy_size2: Double = (pad_x / 2).ceil
+  def dummy_size2: Double = (char_width / 2).ceil
 
   def node_width2(lines: List[String]): Double =
-    (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + pad_x) / 2).ceil
+    (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
 
   def node_height2(num_lines: Int): Double =
-    ((height.ceil * (num_lines max 1) + pad_y) / 2).ceil
+    ((height.ceil * (num_lines max 1) + char_width) / 2).ceil
 
   def level_height2(num_lines: Int, num_edges: Int): Double =
     (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5))