tuned signature;
authorwenzelm
Mon Apr 06 12:51:25 2015 +0200 (2015-04-06 ago)
changeset 59930bdbc4b761c31
parent 59929 a090551e5ec8
child 59931 5ec4f97dd6d4
tuned signature;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 12:37:21 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 12:51:25 2015 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature ISAR_CMD =
     1.6  sig
     1.7 -  val global_setup: Input.source -> theory -> theory
     1.8 +  val setup: Input.source -> theory -> theory
     1.9    val local_setup: Input.source -> Proof.context -> Proof.context
    1.10    val parse_ast_translation: Input.source -> theory -> theory
    1.11    val parse_translation: Input.source -> theory -> theory
    1.12 @@ -57,7 +57,7 @@
    1.13  
    1.14  (* generic setup *)
    1.15  
    1.16 -fun global_setup source =
    1.17 +fun setup source =
    1.18    ML_Lex.read_source false source
    1.19    |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
    1.20      "Context.map_theory setup"
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 06 12:37:21 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 06 12:51:25 2015 +0200
     2.3 @@ -257,11 +257,11 @@
     2.4      (Parse.ML_source >> Isar_Cmd.ml_diag false);
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
     2.8 -    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
     2.9 +  Outer_Syntax.command @{command_spec "setup"} "ML setup for global theory"
    2.10 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
    2.11  
    2.12  val _ =
    2.13 -  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
    2.14 +  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML setup for local theory"
    2.15      (Parse.ML_source >> Isar_Cmd.local_setup);
    2.16  
    2.17  val _ =
    2.18 @@ -913,4 +913,3 @@
    2.19          Toplevel.end_proof (K Proof.end_notepad)));
    2.20  
    2.21  end;
    2.22 -
     3.1 --- a/src/Pure/theory.ML	Mon Apr 06 12:37:21 2015 +0200
     3.2 +++ b/src/Pure/theory.ML	Mon Apr 06 12:51:25 2015 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4    val merge: theory * theory -> theory
     3.5    val merge_list: theory list -> theory
     3.6    val setup: (theory -> theory) -> unit
     3.7 +  val local_setup: (Proof.context -> Proof.context) -> unit
     3.8    val get_markup: theory -> Markup.T
     3.9    val axiom_table: theory -> term Name_Space.table
    3.10    val axiom_space: theory -> Name_Space.T
    3.11 @@ -51,6 +52,7 @@
    3.12    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
    3.13  
    3.14  fun setup f = Context.>> (Context.map_theory f);
    3.15 +fun local_setup f = Context.>> (Context.map_proof f);
    3.16  
    3.17  
    3.18