equal
deleted
inserted
replaced
147 let val setup = add_command name (new_command comment command_parser pos) |
147 let val setup = add_command name (new_command comment command_parser pos) |
148 in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end; |
148 in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end; |
149 |
149 |
150 fun command (name, pos) comment parse = |
150 fun command (name, pos) comment parse = |
151 ((** )@{print} {x = "### Outer_Syntax.command"};( *..NOT yet available*) |
151 ((** )@{print} {x = "### Outer_Syntax.command"};( *..NOT yet available*) |
|
152 (**)writeln "### Outer_Syntax.command";(**) |
152 raw_command (name, pos) comment (Parser parse) |
153 raw_command (name, pos) comment (Parser parse) |
153 ); |
154 ); |
154 |
155 |
155 fun maybe_begin_local_theory command_keyword comment parse_local parse_global = |
156 fun maybe_begin_local_theory command_keyword comment parse_local parse_global = |
156 raw_command command_keyword comment |
157 raw_command command_keyword comment |