prefer fractional font metrics, for proper scaling of node size;
authorwenzelm
Sun, 18 Jan 2015 12:50:36 +0100
changeset 59389 c427f3de9050
parent 59388 04cdfd536e7d
child 59390 7cab7fdf6048
prefer fractional font metrics, for proper scaling of node size;
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)