1.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun May 30 16:54:40 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun May 30 18:23:50 2010 +0200
     1.3 @@ -69,7 +69,16 @@
     1.4  
     1.5  fun token_markup tok =
     1.6    if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
     1.7 -  else token_kind_markup (Token.kind_of tok);
     1.8 +  else
     1.9 +    let
    1.10 +      val kind = Token.kind_of tok;
    1.11 +      val props =
    1.12 +        if kind = Token.Command then
    1.13 +          (case Keyword.command_keyword (Token.content_of tok) of
    1.14 +            SOME k => Markup.properties [(Markup.kindN, Keyword.kind_of k)]
    1.15 +          | NONE => I)
    1.16 +        else I;
    1.17 +    in props (token_kind_markup kind) end;
    1.18  
    1.19  in
    1.20