equal
deleted
inserted
replaced
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 } |