src/Tools/jEdit/patches/folding
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 67993 752a4e6d760c
permissions -rw-r--r--
formal update of patches -- no change of content;
wenzelm@67993
     1
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
wenzelm@67993
     2
--- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-09 01:57:06.000000000 +0200
wenzelm@70019
     3
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2019-02-24 12:20:30.594535134 +0100
wenzelm@67993
     4
@@ -1961,29 +1961,23 @@
wenzelm@58702
     5
 			{
wenzelm@58702
     6
 				Segment seg = new Segment();
wenzelm@58702
     7
 				newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
wenzelm@58702
     8
-				if(newFoldLevel != lineMgr.getFoldLevel(i))
wenzelm@58702
     9
+				if(Debug.FOLD_DEBUG)
wenzelm@58702
    10
+					Log.log(Log.DEBUG,this,i + " fold level changed");
wenzelm@58702
    11
+				changed = true;
wenzelm@58702
    12
+				// Update preceding fold levels if necessary
wenzelm@58702
    13
+				List<Integer> precedingFoldLevels =
wenzelm@58702
    14
+					foldHandler.getPrecedingFoldLevels(
wenzelm@58702
    15
+						this,i,seg,newFoldLevel);
wenzelm@58702
    16
+				if (precedingFoldLevels != null)
wenzelm@58702
    17
 				{
wenzelm@58702
    18
-					if(Debug.FOLD_DEBUG)
wenzelm@58702
    19
-						Log.log(Log.DEBUG,this,i + " fold level changed");
wenzelm@58702
    20
-					changed = true;
wenzelm@58702
    21
-					// Update preceding fold levels if necessary
wenzelm@58702
    22
-					if (i == firstInvalidFoldLevel)
wenzelm@58702
    23
+					int j = i;
wenzelm@58702
    24
+					for (Integer foldLevel: precedingFoldLevels)
wenzelm@58702
    25
 					{
wenzelm@58702
    26
-						List<Integer> precedingFoldLevels =
wenzelm@58702
    27
-							foldHandler.getPrecedingFoldLevels(
wenzelm@58702
    28
-								this,i,seg,newFoldLevel);
wenzelm@58702
    29
-						if (precedingFoldLevels != null)
wenzelm@58702
    30
-						{
wenzelm@58702
    31
-							int j = i;
wenzelm@58702
    32
-							for (Integer foldLevel: precedingFoldLevels)
wenzelm@58702
    33
-							{
wenzelm@58702
    34
-								j--;
wenzelm@58702
    35
-								lineMgr.setFoldLevel(j,foldLevel.intValue());
wenzelm@58702
    36
-							}
wenzelm@58702
    37
-							if (j < firstUpdatedFoldLevel)
wenzelm@58702
    38
-								firstUpdatedFoldLevel = j;
wenzelm@58702
    39
-						}
wenzelm@58702
    40
+						j--;
wenzelm@58702
    41
+						lineMgr.setFoldLevel(j,foldLevel.intValue());
wenzelm@58702
    42
 					}
wenzelm@58702
    43
+					if (j < firstUpdatedFoldLevel)
wenzelm@58702
    44
+						firstUpdatedFoldLevel = j;
wenzelm@58702
    45
 				}
wenzelm@58702
    46
 				lineMgr.setFoldLevel(i,newFoldLevel);
wenzelm@58702
    47
 			}