# HG changeset patch # User wenzelm # Date 1428320062 -7200 # Node ID 74872a13f628c00fc0752d32f6240a39a6a29242 # Parent 5ec4f97dd6d42370089020fbe394dc68191d3e7e support local command setup; diff -r 5ec4f97dd6d4 -r 74872a13f628 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);