src/Tools/VSCode/src/build_vscode.scala
changeset 65251 4b0a43afc3fb
parent 65210 8cfdf420b643
child 65367 83c30e290702
equal deleted inserted replaced
65250:13a6c81534a8 65251:4b0a43afc3fb
    47   /* grammar */
    47   /* grammar */
    48 
    48 
    49   def build_grammar(options: Options, progress: Progress = No_Progress)
    49   def build_grammar(options: Options, progress: Progress = No_Progress)
    50   {
    50   {
    51     val logic = Grammar.default_logic
    51     val logic = Grammar.default_logic
    52     val keywords = Build.session_base(options, logic).syntax.keywords
    52     val keywords = Sessions.session_base(options, logic).syntax.keywords
    53 
    53 
    54     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    54     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    55     progress.echo(output_path.implode)
    55     progress.echo(output_path.implode)
    56     File.write_backup(output_path, Grammar.generate(keywords))
    56     File.write_backup(output_path, Grammar.generate(keywords))
    57   }
    57   }