src/Pure/Isar/token.ML
changeset 65174 c0388fbd8096
parent 64677 8dc24130e8fe
child 66044 bd7516709051
--- a/src/Pure/Isar/token.ML	Fri Mar 10 16:07:20 2017 +0100
+++ b/src/Pure/Isar/token.ML	Fri Mar 10 17:08:21 2017 +0100
@@ -282,9 +282,11 @@
 
 fun command_markups keywords x =
   if Keyword.is_theory_end keywords x then [Markup.keyword2]
-  else 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];
+  else
+    (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)]);
 
 in