author | wenzelm |
Wed, 22 Jun 2011 16:32:36 +0200 | |
changeset 43506 | bf7400573617 |
parent 43482 | ebb90ff55b79 |
permissions | -rw-r--r-- |
43506 | 1 |
diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java |
2 |
--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2011-06-21 01:28:56.000000000 +0200 |
|
3 |
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2011-06-22 16:07:32.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.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java |
|
14 |
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2011-06-21 01:29:10.000000000 +0200 |
|
15 |
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2011-06-22 16:02:07.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.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java |
|
26 |
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 2011-06-21 01:29:10.000000000 +0200 |
|
27 |
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2011-06-22 16:08:47.000000000 +0200 |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
28 |
@@ -57,7 +57,7 @@ |
43506 | 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.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java |
|
38 |
--- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2011-06-21 01:29:11.000000000 +0200 |
|
39 |
+++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2011-06-22 16:05:28.000000000 +0200 |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
40 |
@@ -194,6 +194,23 @@ |
43506 | 41 |
} |
42 |
||
43 |
/** |
|
44 |
+ * Extended styles derived from the user-specified style array. |
|
45 |
+ */ |
|
46 |
+ |
|
47 |
+ public static class StyleExtender |
|
48 |
+ { |
|
49 |
+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
50 |
+ { |
|
51 |
+ return styles; |
|
52 |
+ } |
|
53 |
+ } |
|
54 |
+ volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
55 |
+ public static void setStyleExtender(StyleExtender ext) |
|
56 |
+ { |
|
57 |
+ _styleExtender = ext; |
|
58 |
+ } |
|
59 |
+ |
|
60 |
+ /** |
|
61 |
* Loads the syntax styles from the properties, giving them the specified |
|
62 |
* base font family and size. |
|
63 |
* @param family The font family |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
64 |
@@ -222,8 +239,9 @@ |
43506 | 65 |
Log.log(Log.ERROR,StandardUtilities.class,e); |
66 |
} |
|
67 |
} |
|
68 |
+ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); |
|
69 |
||
70 |
- return styles; |
|
71 |
+ return _styleExtender.extendStyles(styles); |
|
72 |
} //}}} |
|
73 |
||
74 |
private SyntaxUtilities(){} |