--- a/src/Tools/jEdit/src/rendering.scala Sat Feb 15 16:55:48 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Feb 15 17:04:55 2014 +0100
@@ -128,9 +128,9 @@
ML_Lex.Kind.IDENT -> NULL,
ML_Lex.Kind.LONG_IDENT -> NULL,
ML_Lex.Kind.TYPE_VAR -> NULL,
- ML_Lex.Kind.WORD -> NULL,
- ML_Lex.Kind.INT -> NULL,
- ML_Lex.Kind.REAL -> NULL,
+ ML_Lex.Kind.WORD -> DIGIT,
+ ML_Lex.Kind.INT -> DIGIT,
+ ML_Lex.Kind.REAL -> DIGIT,
ML_Lex.Kind.CHAR -> LITERAL2,
ML_Lex.Kind.STRING -> LITERAL1,
ML_Lex.Kind.SPACE -> NULL,