no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
authorwenzelm
Sat, 23 Mar 2013 19:54:15 +0100
changeset 51497 7e8968c9a549
parent 51496 cb677987b7e3
child 51498 979592b765f8
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
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)