# HG changeset patch
# User wenzelm
# Date 1394894963 -3600
# Node ID 331f4aba14b3e63620d47053e5c1a900a62dac77
# Parent  ea6303e2261b2c711fdd6df095fd02353c760ae2
more markup;

diff -r ea6303e2261b -r 331f4aba14b3 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 _ = [];