--- a/src/Pure/Isar/token.ML Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/Isar/token.ML Thu Jun 08 23:04:07 2017 +0200
@@ -293,6 +293,8 @@
fun keyword_markup (important, keyword) x =
if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
+val keyword_properties = Markup.properties [(Markup.kindN, Markup.keywordN)];
+
fun completion_report tok =
if is_kind Keyword tok
then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
@@ -302,7 +304,8 @@
if is_command tok then
keyword_reports tok (command_markups keywords (content_of tok))
else if is_kind Keyword tok then
- keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
+ keyword_reports tok
+ [keyword_markup (false, keyword_properties Markup.keyword2) (content_of tok)]
else
let val (m, text) = token_kind_markup (kind_of tok)
in [((pos_of tok, m), text)] end;