--- 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
}
--- 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)
}