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