tuned;
authorwenzelm
Sat Feb 15 17:04:55 2014 +0100 (2014-02-15 ago)
changeset 55503750206d988ee
parent 55502 72238ea2201c
child 55504 4b6a5068a128
tuned;
src/Tools/jEdit/src/rendering.scala
     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,