src/Tools/jEdit/src/pretty_text_area.scala
changeset 56360 1d122af2b11a
parent 56323 e925118b1875
child 56662 f373fb77e0a4
equal deleted inserted replaced
56359:bca016a9a18d 56360:1d122af2b11a
    83     getPainter.setFont(font)
    83     getPainter.setFont(font)
    84     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    84     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    85     getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
    85     getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
    86     getPainter.setStyles(
    86     getPainter.setStyles(
    87       SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
    87       SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
       
    88 		getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
    88 
    89 
    89     val fold_line_style = new Array[SyntaxStyle](4)
    90     val fold_line_style = new Array[SyntaxStyle](4)
    90     for (i <- 0 to 3) {
    91     for (i <- 0 to 3) {
    91       fold_line_style(i) =
    92       fold_line_style(i) =
    92         SyntaxUtilities.parseStyle(
    93         SyntaxUtilities.parseStyle(