src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 14:13:38 2015 +0100
@@ -132,7 +132,10 @@
     }
 
     def scale_discrete: Double =
-      (scale * visualizer.font_size).floor / visualizer.font_size
+    {
+      val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble
+      (scale * font_height).floor / font_height
+    }
 
     def apply() =
     {