|
1 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java |
|
2 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200 |
|
3 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200 |
|
4 @@ -332,9 +332,9 @@ |
|
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 |
|
16 @@ -584,8 +584,8 @@ |
|
17 // this is either style.getBackgroundColor() or |
|
18 // styles[defaultID].getBackgroundColor() |
|
19 private Color background; |
|
20 - private char[] chars; |
|
21 - private String str; |
|
22 + public char[] chars; |
|
23 + public String str; |
|
24 private GlyphData glyphData; |
|
25 //}}} |
|
26 |
|
27 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java |
|
28 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200 |
|
29 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2021-05-10 18:19:56.275495525 +0200 |
|
30 @@ -914,6 +914,11 @@ |
|
31 return chunkCache.getLineInfo(screenLine).physicalLine; |
|
32 } //}}} |
|
33 |
|
34 + public Chunk getChunksOfScreenLine(int screenLine) |
|
35 + { |
|
36 + return chunkCache.getLineInfo(screenLine).chunks; |
|
37 + } |
|
38 + |
|
39 //{{{ getScreenLineOfOffset() method |
|
40 /** |
|
41 * Returns the screen (wrapped) line containing the specified offset. |
|
42 @@ -1622,8 +1627,8 @@ |
|
43 } |
|
44 |
|
45 // Scan backwards, trying to find a bracket |
|
46 - String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"; |
|
47 - String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"; |
|
48 + String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉"; |
|
49 + String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊"; |
|
50 int count = 1; |
|
51 char openBracket = '\0'; |
|
52 char closeBracket = '\0'; |
|
53 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java |
|
54 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200 |
|
55 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200 |
|
56 @@ -115,6 +115,8 @@ |
|
57 case '⦄': if (direction != null) direction[0] = false; return '⦃'; |
|
58 case '⟪': if (direction != null) direction[0] = true; return '⟫'; |
|
59 case '⟫': if (direction != null) direction[0] = false; return '⟪'; |
|
60 + case '⦉': if (direction != null) direction[0] = true; return '⦊'; |
|
61 + case '⦊': if (direction != null) direction[0] = false; return '⦉'; |
|
62 default: return '\0'; |
|
63 } |
|
64 } //}}} |
|
65 diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java |
|
66 --- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200 |
|
67 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200 |
|
68 @@ -344,8 +344,28 @@ |
|
69 } |
|
70 } |
|
71 |
|
72 - return styles; |
|
73 + styles[0] = |
|
74 + new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK), |
|
75 + null, new Font(family, 0, size)); |
|
76 + return _styleExtender.extendStyles(styles); |
|
77 } //}}} |
|
78 |
|
79 + /** |
|
80 + * Extended styles derived from the user-specified style array. |
|
81 + */ |
|
82 + |
|
83 + public static class StyleExtender |
|
84 + { |
|
85 + public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
86 + { |
|
87 + return styles; |
|
88 + } |
|
89 + } |
|
90 + volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
91 + public static void setStyleExtender(StyleExtender ext) |
|
92 + { |
|
93 + _styleExtender = ext; |
|
94 + } |
|
95 + |
|
96 private SyntaxUtilities(){} |
|
97 } |