--- a/src/Pure/ML/ml_lex.ML Sun May 30 15:27:49 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML Sun May 30 16:00:13 2010 +0200
@@ -88,6 +88,8 @@
(* markup *)
+local
+
val token_kind_markup =
fn Keyword => Markup.ML_keyword
| Ident => Markup.ML_ident
@@ -103,8 +105,16 @@
| Error _ => Markup.ML_malformed
| EOF => Markup.none;
-fun report_token (Token ((pos, _), (kind, _))) =
- Position.report (token_kind_markup kind) pos;
+fun token_markup kind x =
+ if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
+ then Markup.ML_delimiter
+ else token_kind_markup kind;
+
+in
+
+fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
+
+end;