diff -r cc83453fac15 -r 39866de9d988 src/Tools/jEdit/patches/folding --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/folding Sat Oct 18 22:02:10 2014 +0200 @@ -0,0 +1,47 @@ +diff -ru jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java +--- jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2013-07-28 19:03:27.000000000 +0200 ++++ jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2014-10-18 21:35:15.946285279 +0200 +@@ -1945,29 +1945,23 @@ + { + Segment seg = new Segment(); + newFoldLevel = foldHandler.getFoldLevel(this,i,seg); +- if(newFoldLevel != lineMgr.getFoldLevel(i)) ++ if(Debug.FOLD_DEBUG) ++ Log.log(Log.DEBUG,this,i + " fold level changed"); ++ changed = true; ++ // Update preceding fold levels if necessary ++ List precedingFoldLevels = ++ foldHandler.getPrecedingFoldLevels( ++ this,i,seg,newFoldLevel); ++ if (precedingFoldLevels != null) + { +- if(Debug.FOLD_DEBUG) +- Log.log(Log.DEBUG,this,i + " fold level changed"); +- changed = true; +- // Update preceding fold levels if necessary +- if (i == firstInvalidFoldLevel) ++ int j = i; ++ for (Integer foldLevel: precedingFoldLevels) + { +- List precedingFoldLevels = +- foldHandler.getPrecedingFoldLevels( +- this,i,seg,newFoldLevel); +- if (precedingFoldLevels != null) +- { +- int j = i; +- for (Integer foldLevel: precedingFoldLevels) +- { +- j--; +- lineMgr.setFoldLevel(j,foldLevel.intValue()); +- } +- if (j < firstUpdatedFoldLevel) +- firstUpdatedFoldLevel = j; +- } ++ j--; ++ lineMgr.setFoldLevel(j,foldLevel.intValue()); + } ++ if (j < firstUpdatedFoldLevel) ++ firstUpdatedFoldLevel = j; + } + lineMgr.setFoldLevel(i,newFoldLevel); + }