# HG changeset patch
# User wenzelm
# Date 1421581836 -3600
# Node ID c427f3de9050d844cd7e17472a3b2e7a225bce0a
# Parent  04cdfd536e7d8120fa51ef8c98ec29a03ef7362d
prefer fractional font metrics, for proper scaling of node size;

diff -r 04cdfd536e7d -r c427f3de9050 src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala	Sun Jan 18 12:36:25 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Sun Jan 18 12:50:36 2015 +0100
@@ -17,10 +17,15 @@
 object Metrics
 {
   val rendering_hints: RenderingHints =
-    new RenderingHints(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
+  {
+    val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
+    hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
+    hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
+    new RenderingHints(hints)
+  }
 
   val font_render_context: FontRenderContext =
-    new FontRenderContext(null, true, false)
+    new FontRenderContext(null, true, true)
 
   def apply(font: Font): Metrics = new Metrics(font)