src/Pure/Tools/rail.ML
changeset 56163 331f4aba14b3
parent 55828 42ac3cfb89f6
child 56165 dd89ce51d2c8
     1.1 --- a/src/Pure/Tools/rail.ML	Sat Mar 15 12:51:14 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Sat Mar 15 15:49:23 2014 +0100
     1.3 @@ -40,6 +40,8 @@
     1.4  fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
     1.5  
     1.6  fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
     1.7 +  | reports_of_token (Token ((pos, _), (Keyword, x))) =
     1.8 +      map (pair pos) (Markup.keyword3 :: Completion.suppress_abbrevs x)
     1.9    | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
    1.10    | reports_of_token _ = [];
    1.11