# HG changeset patch
# User wenzelm
# Date 1497257890 -7200
# Node ID 7ac97dea27d2f7a9b8766e8f8e514b00ae6283ba
# Parent  1494f3aa819415bef72e4db838ba3f5885260758
tuned signature;

diff -r 1494f3aa8194 -r 7ac97dea27d2 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jun 12 10:51:30 2017 +0200
+++ b/src/Pure/Isar/token.ML	Mon Jun 12 10:58:10 2017 +0200
@@ -286,15 +286,13 @@
     (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
      else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
      else [Markup.keyword1])
-    |> map (Markup.properties [(Markup.kindN, Markup.commandN)]);
+    |> map Markup.command_properties;
 
 in
 
 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))
@@ -305,7 +303,7 @@
     keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
     keyword_reports tok
-      [keyword_markup (false, keyword_properties Markup.keyword2) (content_of tok)]
+      [keyword_markup (false, Markup.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;
diff -r 1494f3aa8194 -r 7ac97dea27d2 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Jun 12 10:51:30 2017 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Jun 12 10:58:10 2017 +0200
@@ -125,8 +125,8 @@
   val markdown_itemN: string val markdown_item: int -> T
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
-  val commandN: string
-  val keywordN: string
+  val commandN: string val command_properties: T -> T
+  val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
@@ -482,8 +482,9 @@
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
-val commandN = "command";
-val keywordN = "keyword";
+val commandN = "command"; val command_properties = properties [(kindN, commandN)];
+val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
+
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";