--- 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"
--- 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;
-
--- 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);