no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
authorwenzelm
Sat Mar 23 19:54:15 2013 +0100 (2013-03-23 ago)
changeset 514977e8968c9a549
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
     1.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 19:39:31 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 19:54:15 2013 +0100
     1.3 @@ -83,6 +83,7 @@
     1.4      val font = new Font(current_font_family, Font.PLAIN, current_font_size)
     1.5      getPainter.setFont(font)
     1.6      getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
     1.7 +    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
     1.8      getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
     1.9  
    1.10      val fold_line_style = new Array[SyntaxStyle](4)