diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-05-20 11:10:12.000000000 +0200
+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-06-10 16:03:10.547355787 +0200
@@ -1968,29 +1968,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);
- }
- if (j < firstUpdatedFoldLevel)
- firstUpdatedFoldLevel = j;
- }
+ j--;
+ lineMgr.setFoldLevel(j, foldLevel);
}
+ if (j < firstUpdatedFoldLevel)
+ firstUpdatedFoldLevel = j;
}
lineMgr.setFoldLevel(i,newFoldLevel);
}