--- 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
--- 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)
})
}