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