|
1 diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java |
|
2 --- 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-20 19:56:05.000000000 +0200 |
|
3 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-23 20:02:22.161225360 +0200 |
|
4 @@ -79,7 +79,7 @@ |
|
5 start = next; |
|
6 token = token.next; |
|
7 } |
|
8 - if (token.id == Token.END || token.id == Token.NULL) |
|
9 + if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL) |
|
10 { |
|
11 JOptionPane.showMessageDialog(textArea.getView(), |
|
12 jEdit.getProperty("syntax-style-no-token.message"), |
|
13 diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java |
|
14 --- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-20 19:56:07.000000000 +0200 |
|
15 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-23 20:02:22.161225360 +0200 |
|
16 @@ -259,9 +259,9 @@ |
|
17 //{{{ Package private members |
|
18 |
|
19 //{{{ Instance variables |
|
20 - SyntaxStyle style; |
|
21 + public SyntaxStyle style; |
|
22 // set up after init() |
|
23 - float width; |
|
24 + public float width; |
|
25 //}}} |
|
26 |
|
27 //{{{ Chunk constructor |
|
28 @@ -509,7 +509,7 @@ |
|
29 // this is either style.getBackgroundColor() or |
|
30 // styles[defaultID].getBackgroundColor() |
|
31 private Color background; |
|
32 - private String str; |
|
33 + public String str; |
|
34 private GlyphVector[] glyphs; |
|
35 //}}} |
|
36 |
|
37 diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java |
|
38 --- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2015-10-20 19:56:07.000000000 +0200 |
|
39 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2015-10-23 20:02:22.161225360 +0200 |
|
40 @@ -57,7 +57,7 @@ |
|
41 */ |
|
42 public static String tokenToString(byte token) |
|
43 { |
|
44 - return (token == Token.END) ? "END" : TOKEN_TYPES[token]; |
|
45 + return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT]; |
|
46 } //}}} |
|
47 |
|
48 //{{{ Token types |
|
49 diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java |
|
50 --- 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-20 19:56:03.000000000 +0200 |
|
51 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-23 20:02:22.161225360 +0200 |
|
52 @@ -910,6 +910,11 @@ |
|
53 return chunkCache.getLineInfo(screenLine).physicalLine; |
|
54 } //}}} |
|
55 |
|
56 + public Chunk getChunksOfScreenLine(int screenLine) |
|
57 + { |
|
58 + return chunkCache.getLineInfo(screenLine).chunks; |
|
59 + } |
|
60 + |
|
61 //{{{ getScreenLineOfOffset() method |
|
62 /** |
|
63 * Returns the screen (wrapped) line containing the specified offset. |
|
64 @@ -1618,8 +1623,8 @@ |
|
65 } |
|
66 |
|
67 // Scan backwards, trying to find a bracket |
|
68 - String openBrackets = "([{"; |
|
69 - String closeBrackets = ")]}"; |
|
70 + String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃"; |
|
71 + String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'"; |
|
72 int count = 1; |
|
73 char openBracket = '\0'; |
|
74 char closeBracket = '\0'; |
|
75 diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java |
|
76 --- 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2015-10-20 19:56:00.000000000 +0200 |
|
77 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2015-10-23 19:46:33.728522904 +0200 |
|
78 @@ -97,6 +97,22 @@ |
|
79 case '}': if (direction != null) direction[0] = false; return '{'; |
|
80 case '<': if (direction != null) direction[0] = true; return '>'; |
|
81 case '>': if (direction != null) direction[0] = false; return '<'; |
|
82 + case '«': if (direction != null) direction[0] = true; return '»'; |
|
83 + case '»': if (direction != null) direction[0] = false; return '«'; |
|
84 + case '‹': if (direction != null) direction[0] = true; return '›'; |
|
85 + case '›': if (direction != null) direction[0] = false; return '‹'; |
|
86 + case '⟨': if (direction != null) direction[0] = true; return '⟩'; |
|
87 + case '⟩': if (direction != null) direction[0] = false; return '⟨'; |
|
88 + case '⌈': if (direction != null) direction[0] = true; return '⌉'; |
|
89 + case '⌉': if (direction != null) direction[0] = false; return '⌈'; |
|
90 + case '⌊': if (direction != null) direction[0] = true; return '⌋'; |
|
91 + case '⌋': if (direction != null) direction[0] = false; return '⌊'; |
|
92 + case '⦇': if (direction != null) direction[0] = true; return '⦈'; |
|
93 + case '⦈': if (direction != null) direction[0] = false; return '⦇'; |
|
94 + case '⟦': if (direction != null) direction[0] = true; return '⟧'; |
|
95 + case '⟧': if (direction != null) direction[0] = false; return '⟦'; |
|
96 + case '⦃': if (direction != null) direction[0] = true; return '⦄'; |
|
97 + case '⦄': if (direction != null) direction[0] = false; return '⦃'; |
|
98 default: return '\0'; |
|
99 } |
|
100 } //}}} |
|
101 diff -ru 5.3.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java |
|
102 --- 5.3.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200 |
|
103 +++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-10-23 20:02:22.161225360 +0200 |
|
104 @@ -194,7 +194,24 @@ |
|
105 { |
|
106 return loadStyles(family,size,true); |
|
107 } |
|
108 - |
|
109 + |
|
110 + /** |
|
111 + * Extended styles derived from the user-specified style array. |
|
112 + */ |
|
113 + |
|
114 + public static class StyleExtender |
|
115 + { |
|
116 + public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
117 + { |
|
118 + return styles; |
|
119 + } |
|
120 + } |
|
121 + volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
122 + public static void setStyleExtender(StyleExtender ext) |
|
123 + { |
|
124 + _styleExtender = ext; |
|
125 + } |
|
126 + |
|
127 /** |
|
128 * Loads the syntax styles from the properties, giving them the specified |
|
129 * base font family and size. |
|
130 @@ -224,9 +241,9 @@ |
|
131 Log.log(Log.ERROR,StandardUtilities.class,e); |
|
132 } |
|
133 } |
|
134 - |
|
135 - return styles; |
|
136 + styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); |
|
137 + return _styleExtender.extendStyles(styles); |
|
138 } //}}} |
|
139 - |
|
140 + |
|
141 private SyntaxUtilities(){} |
|
142 } |