src/Tools/jEdit/patches/folding

always apply precedingFoldLevels, avoid unclear shortcuts;
updated Console.jar 5.1.4;

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);
 			}