|
1 diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java |
|
2 --- 4.5.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2012-03-25 18:51:52.000000000 +0200 |
|
3 +++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2012-03-27 23:30:26.000000000 +0200 |
|
4 @@ -78,7 +78,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 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java |
|
14 --- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2012-03-25 18:52:01.000000000 +0200 |
|
15 +++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2012-03-27 23:31:27.000000000 +0200 |
|
16 @@ -380,7 +380,7 @@ |
|
17 // this is either style.getBackgroundColor() or |
|
18 // styles[defaultID].getBackgroundColor() |
|
19 private Color background; |
|
20 - private String str; |
|
21 + public String str; |
|
22 //private GlyphVector gv; |
|
23 private List<GlyphVector> glyphs; |
|
24 private boolean visible; |
|
25 diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java |
|
26 --- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 2012-03-25 18:52:01.000000000 +0200 |
|
27 +++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2012-03-27 23:30:57.000000000 +0200 |
|
28 @@ -57,7 +57,7 @@ |
|
29 */ |
|
30 public static String tokenToString(byte token) |
|
31 { |
|
32 - return (token == Token.END) ? "END" : TOKEN_TYPES[token]; |
|
33 + return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT]; |
|
34 } //}}} |
|
35 |
|
36 //{{{ Token types |
|
37 diff -ru 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java |
|
38 --- 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2012-03-25 18:52:03.000000000 +0200 |
|
39 +++ 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2012-03-27 23:33:07.000000000 +0200 |
|
40 @@ -194,7 +194,24 @@ |
|
41 { |
|
42 return loadStyles(family,size,true); |
|
43 } |
|
44 - |
|
45 + |
|
46 + /** |
|
47 + * Extended styles derived from the user-specified style array. |
|
48 + */ |
|
49 + |
|
50 + public static class StyleExtender |
|
51 + { |
|
52 + public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
53 + { |
|
54 + return styles; |
|
55 + } |
|
56 + } |
|
57 + volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
58 + public static void setStyleExtender(StyleExtender ext) |
|
59 + { |
|
60 + _styleExtender = ext; |
|
61 + } |
|
62 + |
|
63 /** |
|
64 * Loads the syntax styles from the properties, giving them the specified |
|
65 * base font family and size. |
|
66 @@ -224,9 +241,9 @@ |
|
67 Log.log(Log.ERROR,StandardUtilities.class,e); |
|
68 } |
|
69 } |
|
70 - |
|
71 - return styles; |
|
72 + styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); |
|
73 + return _styleExtender.extendStyles(styles); |
|
74 } //}}} |
|
75 - |
|
76 + |
|
77 private SyntaxUtilities(){} |
|
78 } |