# HG changeset patch
# User wenzelm
# Date 1364064855 -3600
# Node ID 7e8968c9a549a8416c77cfe110dbe35027d52fe7
# Parent  cb677987b7e3deb8a2e5d87e9e7da610eed62734
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

diff -r cb677987b7e3 -r 7e8968c9a549 src/Tools/jEdit/src/pretty_text_area.scala
--- 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)