# HG changeset patch
# User wenzelm
# Date 1430677285 -7200
# Node ID baf2c8fddaa4ee55ddd60f1dd2cb4200ccfba093
# Parent  09377954133b0a160b80be9e052d157aadfe2ca7
proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;

diff -r 09377954133b -r baf2c8fddaa4 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 03 20:04:38 2015 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 03 20:21:25 2015 +0200
@@ -118,7 +118,7 @@
       jEdit.getColorProperty("view.gutter.focusBorderColor"),
       jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
       getPainter.getBackground)
-    getGutter.setFoldPainter(getFoldPainter)
+    getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
     getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
 
     if (getWidth > 0) {