more markup;
authorwenzelm
Sat, 15 Mar 2014 15:49:23 +0100
changeset 56163 331f4aba14b3
parent 56162 ea6303e2261b
child 56164 c7805a88f952
more markup;
src/Pure/Tools/rail.ML
--- 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 _ = [];