--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 23 19:39:31 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 23 19:54:15 2013 +0100
@@ -83,6 +83,7 @@
val font = new Font(current_font_family, Font.PLAIN, current_font_size)
getPainter.setFont(font)
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
+ getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
val fold_line_style = new Array[SyntaxStyle](4)