more literal tokens, e.g. "EX!";
authorwenzelm
Mon May 27 22:25:32 2013 +0200 (2013-05-27)
changeset 52189816c88acd269
parent 52188 2da0033370a0
child 52190 c87b7f26e2c7
more literal tokens, e.g. "EX!";
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Mon May 27 22:00:24 2013 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon May 27 22:25:32 2013 +0200
     1.3 @@ -169,7 +169,9 @@
     1.4  (* markup *)
     1.5  
     1.6  fun literal_markup s =
     1.7 -  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
     1.8 +  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
     1.9 +  then Markup.literal
    1.10 +  else Markup.delimiter;
    1.11  
    1.12  val token_kind_markup =
    1.13   fn TFreeSy => Markup.tfree