src/Tools/jEdit/src/rendering.scala
changeset 55503 750206d988ee
parent 55501 fdde1d62e1fb
child 55505 2a1ca7f6607b
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:55:48 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 17:04:55 2014 +0100
     1.3 @@ -128,9 +128,9 @@
     1.4        ML_Lex.Kind.IDENT -> NULL,
     1.5        ML_Lex.Kind.LONG_IDENT -> NULL,
     1.6        ML_Lex.Kind.TYPE_VAR -> NULL,
     1.7 -      ML_Lex.Kind.WORD -> NULL,
     1.8 -      ML_Lex.Kind.INT -> NULL,
     1.9 -      ML_Lex.Kind.REAL -> NULL,
    1.10 +      ML_Lex.Kind.WORD -> DIGIT,
    1.11 +      ML_Lex.Kind.INT -> DIGIT,
    1.12 +      ML_Lex.Kind.REAL -> DIGIT,
    1.13        ML_Lex.Kind.CHAR -> LITERAL2,
    1.14        ML_Lex.Kind.STRING -> LITERAL1,
    1.15        ML_Lex.Kind.SPACE -> NULL,