--- a/src/Tools/VSCode/src/build_vscode.scala Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala Fri Sep 29 22:12:32 2017 +0200
@@ -20,7 +20,7 @@
def build_grammar(options: Options, progress: Progress = No_Progress)
{
val logic = Grammar.default_logic
- val keywords = Sessions.session_base(options, logic).syntax.keywords
+ val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
progress.echo(output_path.implode)