# HG changeset patch # User wenzelm # Date 1396436581 -7200 # Node ID 1d122af2b11a4a5798ad16f92bfaf418a98076d3 # Parent bca016a9a18d9b66dee64064c35b9dc2890f934f observe extra line spacing for output as well; diff -r bca016a9a18d -r 1d122af2b11a src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Apr 02 12:26:11 2014 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Apr 02 13:03:01 2014 +0200 @@ -85,6 +85,7 @@ getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics")) getPainter.setStyles( SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round)) + getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0)) val fold_line_style = new Array[SyntaxStyle](4) for (i <- 0 to 3) {