src/Tools/jEdit/patches/folding

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/folding	Sat Oct 18 22:02:10 2014 +0200
@@ -0,0 +1,47 @@
+diff -ru jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2013-07-28 19:03:27.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2014-10-18 21:35:15.946285279 +0200
+@@ -1945,29 +1945,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);
+ 			}