src/Pure/Syntax/lexicon.ML
changeset 52190 c87b7f26e2c7
parent 52189 816c88acd269
child 52616 3ac2878764f9
equal deleted inserted replaced
52184:d6627b50b131 52190:c87b7f26e2c7
   167 
   167 
   168 
   168 
   169 (* markup *)
   169 (* markup *)
   170 
   170 
   171 fun literal_markup s =
   171 fun literal_markup s =
   172   if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
   172   if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
       
   173   then Markup.literal
       
   174   else Markup.delimiter;
   173 
   175 
   174 val token_kind_markup =
   176 val token_kind_markup =
   175  fn TFreeSy => Markup.tfree
   177  fn TFreeSy => Markup.tfree
   176   | TVarSy  => Markup.tvar
   178   | TVarSy  => Markup.tvar
   177   | NumSy   => Markup.numeral
   179   | NumSy   => Markup.numeral