src/Pure/Thy/thy_syntax.ML
changeset 42290 b1f544c84040
parent 41484 51310e1ccd6f
child 43430 1ed88ddf1268
equal deleted inserted replaced
42289:dafae095d733 42290:b1f544c84040
    63   | Token.Error _       => Markup.malformed
    63   | Token.Error _       => Markup.malformed
    64   | Token.Sync          => Markup.control
    64   | Token.Sync          => Markup.control
    65   | Token.EOF           => Markup.control;
    65   | Token.EOF           => Markup.control;
    66 
    66 
    67 fun token_markup tok =
    67 fun token_markup tok =
    68   if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
    68   if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator
    69   else
    69   else
    70     let
    70     let
    71       val kind = Token.kind_of tok;
    71       val kind = Token.kind_of tok;
    72       val props =
    72       val props =
    73         if kind = Token.Command
    73         if kind = Token.Command