src/Tools/VSCode/src/build_vscode.scala
changeset 72767 f6bf65554764
parent 72763 3cc73d00553c
child 73340 0ffcad1f6130
equal deleted inserted replaced
72766:47ffeb3448f4 72767:f6bf65554764
    17 
    17 
    18   /* grammar */
    18   /* grammar */
    19 
    19 
    20   def build_grammar(options: Options, progress: Progress = new Progress)
    20   def build_grammar(options: Options, progress: Progress = new Progress)
    21   {
    21   {
    22     val logic = Grammar.default_logic
    22     val logic = TextMate_Grammar.default_logic
    23     val keywords = Sessions.base_info(options, logic).check.base.overall_syntax.keywords
    23     val keywords = Sessions.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(TextMate_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, TextMate_Grammar.generate(keywords))
    28   }
    28   }
    29 
    29 
    30 
    30 
    31   /* extension */
    31   /* extension */
    32 
    32