diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
--- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2018-04-09 01:57:06.000000000 +0200
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2019-02-24 12:20:30.594535134 +0100
@@ -1961,29 +1961,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<Integer> 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<Integer> 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);
}