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