author | wenzelm |
Mon, 20 Jun 2011 22:43:56 +0200 | |
changeset 43482 | ebb90ff55b79 |
parent 43460 | 2852f309174a |
child 43506 | bf7400573617 |
permissions | -rw-r--r-- |
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
1 |
Only in jEdit-patched: build |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
2 |
diff -ru jEdit/org/gjt/sp/jedit/Buffer.java jEdit-patched/org/gjt/sp/jedit/Buffer.java |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
3 |
--- jEdit/org/gjt/sp/jedit/Buffer.java 2010-05-09 14:29:25.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
4 |
+++ jEdit-patched/org/gjt/sp/jedit/Buffer.java 2011-06-18 18:28:19.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
5 |
@@ -2232,7 +2232,7 @@ |
43446
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
6 |
start = next; |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
7 |
token = token.next; |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
8 |
} |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
9 |
- if (token.id == Token.END || token.id == Token.NULL) |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
10 |
+ if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL) |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
11 |
{ |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
12 |
JOptionPane.showMessageDialog(jEdit.getActiveView(), |
9064e1a72c5d
Buffer.editSyntaxStyle: mask extended syntax styles;
wenzelm
parents:
43394
diff
changeset
|
13 |
jEdit.getProperty("syntax-style-no-token.message"), |
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
14 |
diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
15 |
--- jEdit/org/gjt/sp/jedit/syntax/Token.java 2010-05-09 14:29:24.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
16 |
+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2011-06-18 18:28:10.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
17 |
@@ -57,7 +57,7 @@ |
43394 | 18 |
*/ |
19 |
public static String tokenToString(byte token) |
|
20 |
{ |
|
21 |
- return (token == Token.END) ? "END" : TOKEN_TYPES[token]; |
|
22 |
+ return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT]; |
|
23 |
} //}}} |
|
24 |
||
25 |
//{{{ Token types |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
26 |
diff -ru jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
27 |
--- jEdit/org/gjt/sp/util/SyntaxUtilities.java 2010-05-09 14:29:29.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
28 |
+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2011-06-20 21:30:58.000000000 +0200 |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
29 |
@@ -194,6 +194,23 @@ |
43394 | 30 |
} |
31 |
||
32 |
/** |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
33 |
+ * Extended styles derived from the user-specified style array. |
43394 | 34 |
+ */ |
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
35 |
+ |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
36 |
+ public static class StyleExtender |
43394 | 37 |
+ { |
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
38 |
+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
39 |
+ { |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
40 |
+ return styles; |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
41 |
+ } |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
42 |
+ } |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
43 |
+ volatile private static StyleExtender _styleExtender = new StyleExtender(); |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
44 |
+ public static void setStyleExtender(StyleExtender ext) |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
45 |
+ { |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
46 |
+ _styleExtender = ext; |
43394 | 47 |
+ } |
43460 | 48 |
+ |
43394 | 49 |
+ /** |
50 |
* Loads the syntax styles from the properties, giving them the specified |
|
51 |
* base font family and size. |
|
52 |
* @param family The font family |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
53 |
@@ -222,8 +239,9 @@ |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
54 |
Log.log(Log.ERROR,StandardUtilities.class,e); |
43394 | 55 |
} |
56 |
} |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
57 |
+ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); |
43394 | 58 |
|
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
59 |
- return styles; |
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
60 |
+ return _styleExtender.extendStyles(styles); |
43394 | 61 |
} //}}} |
62 |
||
43482
ebb90ff55b79
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents:
43460
diff
changeset
|
63 |
private SyntaxUtilities(){} |