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