Quelle  folding   Sprache: unbekannt

diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-10-29 11:50:54.062016616 +0100
@@ -2054,29 +2054,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);
    }