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