# HG changeset patch
# User wenzelm
# Date 1489162101 -3600
# Node ID c0388fbd80964a27c463321d056b386d85664524
# Parent  3700be571a01d902080aa98c5a4e34a1b7850a28
avoid extra decorations for regular command keywords;

diff -r 3700be571a01 -r c0388fbd8096 src/Pure/Isar/token.ML
--- 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
 
diff -r 3700be571a01 -r c0388fbd8096 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 16:07:20 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 17:08:21 2017 +0100
@@ -117,7 +117,9 @@
   {
     snapshot.select(range, Rendering.text_color_elements, _ =>
       {
-        case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
+        case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
+          if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
+          else Rendering.text_color.get(name)
       })
   }