# HG changeset patch
# User wenzelm
# Date 1413662530 -7200
# Node ID 39866de9d9884e448b269ce9ff74c39a8f4a68d7
# Parent  cc83453fac1504d2764bfc8db7080e81c3563f17
always apply precedingFoldLevels, avoid unclear shortcuts;
updated Console.jar 5.1.4;

diff -r cc83453fac15 -r 39866de9d988 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sat Oct 18 21:26:01 2014 +0200
+++ b/Admin/components/components.sha1	Sat Oct 18 22:02:10 2014 +0200
@@ -56,6 +56,7 @@
 054c1300128f8abd0f46a3e92c756ccdb96ff2af  jedit_build-20140405.tar.gz
 4a963665537ea66c69de4d761846541ebdbf69f2  jedit_build-20140511.tar.gz
 a9d637a30f6a87a3583f265da51e63e3619cff52  jedit_build-20140722.tar.gz
+f29391c53d85715f8454e1aaa304fbccc352928f  jedit_build-20141018.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
diff -r cc83453fac15 -r 39866de9d988 Admin/components/main
--- a/Admin/components/main	Sat Oct 18 21:26:01 2014 +0200
+++ b/Admin/components/main	Sat Oct 18 22:02:10 2014 +0200
@@ -5,7 +5,7 @@
 exec_process-1.0.3
 Haskabelle-2014
 jdk-7u67
-jedit_build-20140722
+jedit_build-20141018
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
diff -r cc83453fac15 -r 39866de9d988 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);
+ 			}