src/Tools/VSCode/src/build_vscode.scala
changeset 66964 9f2de457b95e
parent 66963 1c3d0c12bb51
child 66976 806bc39550a5
equal deleted inserted replaced
66963:1c3d0c12bb51 66964:9f2de457b95e
    18   /* grammar */
    18   /* grammar */
    19 
    19 
    20   def build_grammar(options: Options, progress: Progress = No_Progress)
    20   def build_grammar(options: Options, progress: Progress = No_Progress)
    21   {
    21   {
    22     val logic = Grammar.default_logic
    22     val logic = Grammar.default_logic
    23     val keywords = Sessions.session_base_info(options, logic).check.overall_syntax.keywords
    23     val keywords = Sessions.session_base_info(options, logic).check_base.overall_syntax.keywords
    24 
    24 
    25     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    25     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    26     progress.echo(output_path.implode)
    26     progress.echo(output_path.implode)
    27     File.write_backup(output_path, Grammar.generate(keywords))
    27     File.write_backup(output_path, Grammar.generate(keywords))
    28   }
    28   }