support local command setup;
authorwenzelm
Mon Apr 06 13:34:22 2015 +0200 (2015-04-06)
changeset 5993274872a13f628
parent 59931 5ec4f97dd6d4
child 59933 07a7544c0535
support local command setup;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 13:28:54 2015 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 13:34:22 2015 +0200
     1.3 @@ -137,7 +137,8 @@
     1.4  type command_spec = string * Position.T;
     1.5  
     1.6  fun raw_command (name, pos) comment command_parser =
     1.7 -  Theory.setup (add_command name (new_command comment command_parser pos));
     1.8 +  let val setup = add_command name (new_command comment command_parser pos)
     1.9 +  in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
    1.10  
    1.11  fun command (name, pos) comment parse =
    1.12    raw_command (name, pos) comment (Parser parse);