| author | wenzelm | 
| Wed, 29 Jan 2025 20:17:21 +0100 | |
| changeset 82015 | fe186fd7a168 | 
| parent 81297 | 07f64697408e | 
| child 82181 | a0d1d772ccab | 
| permissions | -rw-r--r-- | 
| 81297 | 1  | 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java  | 
2  | 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200  | 
|
3  | 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100  | 
|
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
4  | 
@@ -332,9 +332,9 @@  | 
| 50306 | 5  | 
 	//{{{ Package private members
 | 
6  | 
||
7  | 
 	//{{{ Instance variables
 | 
|
8  | 
- SyntaxStyle style;  | 
|
9  | 
+ public SyntaxStyle style;  | 
|
10  | 
// set up after init()  | 
|
11  | 
- float width;  | 
|
12  | 
+ public float width;  | 
|
13  | 
//}}}  | 
|
14  | 
||
15  | 
 	//{{{ Chunk constructor
 | 
|
| 72247 | 16  | 
@@ -584,8 +584,8 @@  | 
17  | 
// this is either style.getBackgroundColor() or  | 
|
| 48786 | 18  | 
// styles[defaultID].getBackgroundColor()  | 
19  | 
private Color background;  | 
|
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
20  | 
- private char[] chars;  | 
| 48786 | 21  | 
- private String str;  | 
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
22  | 
+ public char[] chars;  | 
| 48786 | 23  | 
+ public String str;  | 
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
24  | 
private GlyphData glyphData;  | 
| 50306 | 25  | 
//}}}  | 
26  | 
||
| 
80156
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
27  | 
@@ -926,6 +926,11 @@  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
28  | 
}  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
29  | 
|
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
30  | 
@Override  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
31  | 
+		public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
 | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
32  | 
+			synchronized (this) { return super.computeIfAbsent(key, f); }
 | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
33  | 
+ }  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
34  | 
+  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
35  | 
+ @Override  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
36  | 
protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)  | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
37  | 
 		{
 | 
| 
 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 
wenzelm 
parents: 
79012 
diff
changeset
 | 
38  | 
return size() > capacity;  | 
| 81297 | 39  | 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java  | 
40  | 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200  | 
|
41  | 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-10-29 11:50:54.066016546 +0100  | 
|
42  | 
@@ -919,6 +919,11 @@  | 
|
| 61511 | 43  | 
return chunkCache.getLineInfo(screenLine).physicalLine;  | 
44  | 
} //}}}  | 
|
45  | 
||
46  | 
+ public Chunk getChunksOfScreenLine(int screenLine)  | 
|
47  | 
+        {
 | 
|
48  | 
+ return chunkCache.getLineInfo(screenLine).chunks;  | 
|
49  | 
+ }  | 
|
50  | 
+  | 
|
51  | 
 	//{{{ getScreenLineOfOffset() method
 | 
|
52  | 
/**  | 
|
53  | 
* Returns the screen (wrapped) line containing the specified offset.  | 
|
| 81297 | 54  | 
@@ -1627,8 +1632,8 @@  | 
| 73658 | 55  | 
}  | 
56  | 
||
57  | 
// Scan backwards, trying to find a bracket  | 
|
58  | 
-		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
 | 
|
59  | 
- String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";  | 
|
60  | 
+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
 | 
|
61  | 
+ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊";  | 
|
62  | 
int count = 1;  | 
|
63  | 
char openBracket = '\0';  | 
|
64  | 
char closeBracket = '\0';  | 
|
| 81297 | 65  | 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java  | 
66  | 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200  | 
|
67  | 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100  | 
|
| 73658 | 68  | 
@@ -115,6 +115,8 @@  | 
69  | 
case '⦄': if (direction != null) direction[0] = false; return '⦃';  | 
|
70  | 
case '⟪': if (direction != null) direction[0] = true; return '⟫';  | 
|
71  | 
case '⟫': if (direction != null) direction[0] = false; return '⟪';  | 
|
72  | 
+ case '⦉': if (direction != null) direction[0] = true; return '⦊';  | 
|
73  | 
+ case '⦊': if (direction != null) direction[0] = false; return '⦉';  | 
|
74  | 
default: return '\0';  | 
|
75  | 
}  | 
|
76  | 
} //}}}  | 
|
| 81297 | 77  | 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java  | 
78  | 
--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200  | 
|
79  | 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-10-29 11:50:54.066016546 +0100  | 
|
80  | 
@@ -357,8 +357,28 @@  | 
|
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
81  | 
}  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
82  | 
}  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
83  | 
|
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
84  | 
- return styles;  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
85  | 
+ styles[0] =  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
86  | 
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
 | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
87  | 
+ null, new Font(family, 0, size));  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
88  | 
+ return _styleExtender.extendStyles(styles);  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
89  | 
} //}}}  | 
| 
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
90  | 
|
| 48786 | 91  | 
+ /**  | 
92  | 
+ * Extended styles derived from the user-specified style array.  | 
|
93  | 
+ */  | 
|
94  | 
+  | 
|
95  | 
+ public static class StyleExtender  | 
|
96  | 
+	{
 | 
|
97  | 
+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)  | 
|
98  | 
+		{
 | 
|
99  | 
+ return styles;  | 
|
100  | 
+ }  | 
|
101  | 
+ }  | 
|
102  | 
+ volatile private static StyleExtender _styleExtender = new StyleExtender();  | 
|
103  | 
+ public static void setStyleExtender(StyleExtender ext)  | 
|
104  | 
+	{
 | 
|
105  | 
+ _styleExtender = ext;  | 
|
106  | 
+ }  | 
|
107  | 
+  | 
|
108  | 
 	private SyntaxUtilities(){}
 | 
|
109  | 
}  |