localized command 'method_setup' and 'attribute_setup';
authorwenzelm
Thu Aug 14 14:28:11 2014 +0200 (2014-08-14)
changeset 5794157200bdc2aa7
parent 57940 ca3be9612d85
child 57942 e5bec882fdd0
localized command 'method_setup' and 'attribute_setup';
clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Spec.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/method.ML
     1.1 --- a/NEWS	Thu Aug 14 12:49:49 2014 +0200
     1.2 +++ b/NEWS	Thu Aug 14 14:28:11 2014 +0200
     1.3 @@ -4,6 +4,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Commands 'method_setup' and 'attribute_setup' now work within a
    1.10 +local theory context.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Sledgehammer:
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 12:49:49 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 14:28:11 2014 +0200
     2.3 @@ -915,7 +915,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.9    \end{matharray}
    2.10  
    2.11    @{rail \<open>
    2.12 @@ -925,7 +925,7 @@
    2.13    \begin{description}
    2.14  
    2.15    \item @{command "method_setup"}~@{text "name = text description"}
    2.16 -  defines a proof method in the current theory.  The given @{text
    2.17 +  defines a proof method in the current context.  The given @{text
    2.18    "text"} has to be an ML expression of type
    2.19    @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
    2.20    basic parsers defined in structure @{ML_structure Args} and @{ML_structure
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 12:49:49 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 14:28:11 2014 +0200
     3.3 @@ -1031,7 +1031,7 @@
     3.4      @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     3.5      @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     3.6      @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.7 -    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     3.8 +    @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.9    \end{matharray}
    3.10    \begin{tabular}{rcll}
    3.11      @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
    3.12 @@ -1093,7 +1093,7 @@
    3.13    concrete outer syntax, for example.
    3.14  
    3.15    \item @{command "attribute_setup"}~@{text "name = text description"}
    3.16 -  defines an attribute in the current theory.  The given @{text
    3.17 +  defines an attribute in the current context.  The given @{text
    3.18    "text"} has to be an ML expression of type
    3.19    @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
    3.20    structure @{ML_structure Args} and @{ML_structure Attrib}.
     4.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 12:49:49 2014 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 14:28:11 2014 +0200
     4.3 @@ -42,7 +42,8 @@
     4.4    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     4.5    val local_setup: Binding.binding -> attribute context_parser -> string ->
     4.6      local_theory -> local_theory
     4.7 -  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
     4.8 +  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     4.9 +    local_theory -> local_theory
    4.10    val internal: (morphism -> attribute) -> src
    4.11    val add_del: attribute -> attribute -> attribute context_parser
    4.12    val thm_sel: Facts.interval list parser
    4.13 @@ -132,15 +133,12 @@
    4.14        Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
    4.15    in (name, Context.the_theory (Attributes.put attribs' context)) end;
    4.16  
    4.17 -fun define binding att comment lthy =
    4.18 -  let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in
    4.19 -    lthy
    4.20 -    |> Local_Theory.background_theory_result (define_global binding att0 comment)
    4.21 -    |-> (fn name =>
    4.22 -      Local_Theory.map_contexts (K transfer_attributes)
    4.23 -      #> Local_Theory.generic_alias Attributes.map binding name
    4.24 -      #> pair name)
    4.25 -  end;
    4.26 +fun define binding att comment =
    4.27 +  Local_Theory.background_theory_result (define_global binding att comment)
    4.28 +  #-> (fn name =>
    4.29 +    Local_Theory.map_contexts (K transfer_attributes)
    4.30 +    #> Local_Theory.generic_alias Attributes.map binding name
    4.31 +    #> pair name);
    4.32  
    4.33  
    4.34  (* check *)
    4.35 @@ -207,12 +205,13 @@
    4.36  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
    4.37  
    4.38  fun attribute_setup name source cmt =
    4.39 -  Context.theory_map (ML_Context.expression (#pos source)
    4.40 +  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    4.41 +    ML_Lex.read_source false source @
    4.42 +    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    4.43 +  |> ML_Context.expression (#pos source)
    4.44      "val (name, scan, comment): binding * attribute context_parser * string"
    4.45 -    "Context.map_theory (Attrib.setup name scan comment)"
    4.46 -    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    4.47 -      ML_Lex.read_source false source @
    4.48 -      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    4.49 +    "Context.map_proof (Attrib.local_setup name scan comment)"
    4.50 +  |> Context.proof_map;
    4.51  
    4.52  
    4.53  (* internal attribute *)
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Aug 14 12:49:49 2014 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 14:28:11 2014 +0200
     5.3 @@ -329,16 +329,16 @@
     5.4      (Parse.ML_source >> Isar_Cmd.local_setup);
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
     5.8 +  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
     5.9      (Parse.position Parse.name --
    5.10          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
    5.11 -      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
    5.12 +      >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
    5.13  
    5.14  val _ =
    5.15 -  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
    5.16 +  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
    5.17      (Parse.position Parse.name --
    5.18          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
    5.19 -      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    5.20 +      >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
    5.21  
    5.22  val _ =
    5.23    Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
     6.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:49:49 2014 +0200
     6.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 14:28:11 2014 +0200
     6.3 @@ -39,7 +39,6 @@
     6.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     6.5    val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     6.6    val background_theory: (theory -> theory) -> local_theory -> local_theory
     6.7 -  val background_morphism: local_theory -> morphism
     6.8    val target_of: local_theory -> Proof.context
     6.9    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    6.10    val target_morphism: local_theory -> morphism
    6.11 @@ -106,7 +105,8 @@
    6.12    target: Proof.context};
    6.13  
    6.14  fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
    6.15 -  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
    6.16 +  {naming = naming, operations = operations, after_close = after_close,
    6.17 +    brittle = brittle, target = target};
    6.18  
    6.19  
    6.20  (* context data *)
    6.21 @@ -226,9 +226,6 @@
    6.22  
    6.23  fun background_theory f = #2 o background_theory_result (f #> pair ());
    6.24  
    6.25 -fun background_morphism lthy =
    6.26 -  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    6.27 -
    6.28  
    6.29  (* target contexts *)
    6.30  
     7.1 --- a/src/Pure/Isar/method.ML	Thu Aug 14 12:49:49 2014 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 14 14:28:11 2014 +0200
     7.3 @@ -70,7 +70,8 @@
     7.4    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
     7.5    val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     7.6      local_theory -> local_theory
     7.7 -  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
     7.8 +  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     7.9 +    local_theory -> local_theory
    7.10    type modifier = (Proof.context -> Proof.context) * attribute
    7.11    val section: modifier parser list -> thm list context_parser
    7.12    val sections: modifier parser list -> thm list list context_parser
    7.13 @@ -350,15 +351,12 @@
    7.14        Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
    7.15    in (name, Context.the_theory (Methods.put meths' context)) end;
    7.16  
    7.17 -fun define binding meth comment lthy =
    7.18 -  let val meth0 = meth o Args.transform_values (Local_Theory.background_morphism lthy) in
    7.19 -    lthy
    7.20 -    |> Local_Theory.background_theory_result (define_global binding meth0 comment)
    7.21 -    |-> (fn name =>
    7.22 -      Local_Theory.map_contexts (K transfer_methods)
    7.23 -      #> Local_Theory.generic_alias Methods.map binding name
    7.24 -      #> pair name)
    7.25 -  end;
    7.26 +fun define binding meth comment =
    7.27 +  Local_Theory.background_theory_result (define_global binding meth comment)
    7.28 +  #-> (fn name =>
    7.29 +    Local_Theory.map_contexts (K transfer_methods)
    7.30 +    #> Local_Theory.generic_alias Methods.map binding name
    7.31 +    #> pair name);
    7.32  
    7.33  
    7.34  (* check *)
    7.35 @@ -393,12 +391,13 @@
    7.36  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
    7.37  
    7.38  fun method_setup name source cmt =
    7.39 -  Context.theory_map (ML_Context.expression (#pos source)
    7.40 +  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    7.41 +    ML_Lex.read_source false source @
    7.42 +    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    7.43 +  |> ML_Context.expression (#pos source)
    7.44      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    7.45 -    "Context.map_theory (Method.setup name scan comment)"
    7.46 -    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    7.47 -      ML_Lex.read_source false source @
    7.48 -      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    7.49 +    "Context.map_proof (Method.local_setup name scan comment)"
    7.50 +  |> Context.proof_map;
    7.51  
    7.52  
    7.53