# HG changeset patch # User wenzelm # Date 1428317485 -7200 # Node ID bdbc4b761c319ba96112ea7f5c3653d9a02bb30f # Parent a090551e5ec8fbd37e0153ea1d0713b86d27d57f tuned signature; diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Apr 06 12:37:21 2015 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Apr 06 12:51:25 2015 +0200 @@ -6,7 +6,7 @@ signature ISAR_CMD = sig - val global_setup: Input.source -> theory -> theory + val setup: Input.source -> theory -> theory val local_setup: Input.source -> Proof.context -> Proof.context val parse_ast_translation: Input.source -> theory -> theory val parse_translation: Input.source -> theory -> theory @@ -57,7 +57,7 @@ (* generic setup *) -fun global_setup source = +fun setup source = ML_Lex.read_source false source |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory" "Context.map_theory setup" diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Apr 06 12:37:21 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Apr 06 12:51:25 2015 +0200 @@ -257,11 +257,11 @@ (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = - Outer_Syntax.command @{command_spec "setup"} "ML theory setup" - (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup)); + Outer_Syntax.command @{command_spec "setup"} "ML setup for global theory" + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = - Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup" + Outer_Syntax.local_theory @{command_spec "local_setup"} "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = @@ -913,4 +913,3 @@ Toplevel.end_proof (K Proof.end_notepad))); end; - diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/theory.ML --- a/src/Pure/theory.ML Mon Apr 06 12:37:21 2015 +0200 +++ b/src/Pure/theory.ML Mon Apr 06 12:51:25 2015 +0200 @@ -14,6 +14,7 @@ val merge: theory * theory -> theory val merge_list: theory list -> theory val setup: (theory -> theory) -> unit + val local_setup: (Proof.context -> Proof.context) -> unit val get_markup: theory -> Markup.T val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T @@ -51,6 +52,7 @@ | merge_list (thy :: thys) = Library.foldl merge (thy, thys); fun setup f = Context.>> (Context.map_theory f); +fun local_setup f = Context.>> (Context.map_proof f);