# HG changeset patch
# User wenzelm
# Date 1369686332 -7200
# Node ID 816c88acd2698420ec39d3f4bbd0d30de292303d
# Parent  2da0033370a0ba7b6a714708437013b066a2ffd6
more literal tokens, e.g. "EX!";

diff -r 2da0033370a0 -r 816c88acd269 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon May 27 22:00:24 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon May 27 22:25:32 2013 +0200
@@ -169,7 +169,9 @@
 (* markup *)
 
 fun literal_markup s =
-  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
+  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
+  then Markup.literal
+  else Markup.delimiter;
 
 val token_kind_markup =
  fn TFreeSy => Markup.tfree