# HG changeset patch
# User wenzelm
# Date 1392480295 -3600
# Node ID 750206d988ee8a9e2747fe8b1fb104ab79368eea
# Parent  72238ea2201cbca42c9ef4b9ddd9d0471f6fe27c
tuned;

diff -r 72238ea2201c -r 750206d988ee src/Tools/jEdit/src/rendering.scala
--- 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,