# HG changeset patch # User wenzelm # Date 1408019291 -7200 # Node ID 57200bdc2aa78072059ea86e1adbeccab5d656ea # Parent ca3be9612d851d9152c36c3457437a9ccefb0c47 localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed; diff -r ca3be9612d85 -r 57200bdc2aa7 NEWS --- a/NEWS Thu Aug 14 12:49:49 2014 +0200 +++ b/NEWS Thu Aug 14 14:28:11 2014 +0200 @@ -4,6 +4,12 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Commands 'method_setup' and 'attribute_setup' now work within a +local theory context. + + *** HOL *** * Sledgehammer: diff -r ca3be9612d85 -r 57200bdc2aa7 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Thu Aug 14 14:28:11 2014 +0200 @@ -915,7 +915,7 @@ text {* \begin{matharray}{rcl} - @{command_def "method_setup"} & : & @{text "theory \ theory"} \\ + @{command_def "method_setup"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} @{rail \ @@ -925,7 +925,7 @@ \begin{description} \item @{command "method_setup"}~@{text "name = text description"} - defines a proof method in the current theory. The given @{text + defines a proof method in the current context. The given @{text "text"} has to be an ML expression of type @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\ basic parsers defined in structure @{ML_structure Args} and @{ML_structure diff -r ca3be9612d85 -r 57200bdc2aa7 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Thu Aug 14 14:28:11 2014 +0200 @@ -1031,7 +1031,7 @@ @{command_def "ML_command"} & : & @{text "any \"} \\ @{command_def "setup"} & : & @{text "theory \ theory"} \\ @{command_def "local_setup"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "attribute_setup"} & : & @{text "theory \ theory"} \\ + @{command_def "attribute_setup"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} \begin{tabular}{rcll} @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ @@ -1093,7 +1093,7 @@ concrete outer syntax, for example. \item @{command "attribute_setup"}~@{text "name = text description"} - defines an attribute in the current theory. The given @{text + defines an attribute in the current context. The given @{text "text"} has to be an ML expression of type @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in structure @{ML_structure Args} and @{ML_structure Attrib}. diff -r ca3be9612d85 -r 57200bdc2aa7 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Aug 14 14:28:11 2014 +0200 @@ -42,7 +42,8 @@ val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory val local_setup: Binding.binding -> attribute context_parser -> string -> local_theory -> local_theory - val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory + val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> + local_theory -> local_theory val internal: (morphism -> attribute) -> src val add_del: attribute -> attribute -> attribute context_parser val thm_sel: Facts.interval list parser @@ -132,15 +133,12 @@ Name_Space.define context true (binding, (att, comment)) (Attributes.get context); in (name, Context.the_theory (Attributes.put attribs' context)) end; -fun define binding att comment lthy = - let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in - lthy - |> Local_Theory.background_theory_result (define_global binding att0 comment) - |-> (fn name => - Local_Theory.map_contexts (K transfer_attributes) - #> Local_Theory.generic_alias Attributes.map binding name - #> pair name) - end; +fun define binding att comment = + Local_Theory.background_theory_result (define_global binding att comment) + #-> (fn name => + Local_Theory.map_contexts (K transfer_attributes) + #> Local_Theory.generic_alias Attributes.map binding name + #> pair name); (* check *) @@ -207,12 +205,13 @@ fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; fun attribute_setup name source cmt = - Context.theory_map (ML_Context.expression (#pos source) + (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ + ML_Lex.read_source false source @ + ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) + |> ML_Context.expression (#pos source) "val (name, scan, comment): binding * attribute context_parser * string" - "Context.map_theory (Attrib.setup name scan comment)" - (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read_source false source @ - ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))); + "Context.map_proof (Attrib.local_setup name scan comment)" + |> Context.proof_map; (* internal attribute *) diff -r ca3be9612d85 -r 57200bdc2aa7 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Aug 14 14:28:11 2014 +0200 @@ -329,16 +329,16 @@ (Parse.ML_source >> Isar_Cmd.local_setup); val _ = - Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML" + Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML" (Parse.position Parse.name -- Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "") - >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt))); + >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = - Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML" + Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML" (Parse.position Parse.name -- Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "") - >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); + >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration" diff -r ca3be9612d85 -r 57200bdc2aa7 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Pure/Isar/local_theory.ML Thu Aug 14 14:28:11 2014 +0200 @@ -39,7 +39,6 @@ val raw_theory: (theory -> theory) -> local_theory -> local_theory val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val background_theory: (theory -> theory) -> local_theory -> local_theory - val background_morphism: local_theory -> morphism val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism @@ -106,7 +105,8 @@ target: Proof.context}; fun make_lthy (naming, operations, after_close, brittle, target) : lthy = - {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target}; + {naming = naming, operations = operations, after_close = after_close, + brittle = brittle, target = target}; (* context data *) @@ -226,9 +226,6 @@ fun background_theory f = #2 o background_theory_result (f #> pair ()); -fun background_morphism lthy = - standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy)); - (* target contexts *) diff -r ca3be9612d85 -r 57200bdc2aa7 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Aug 14 12:49:49 2014 +0200 +++ b/src/Pure/Isar/method.ML Thu Aug 14 14:28:11 2014 +0200 @@ -70,7 +70,8 @@ val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val local_setup: binding -> (Proof.context -> method) context_parser -> string -> local_theory -> local_theory - val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory + val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> + local_theory -> local_theory type modifier = (Proof.context -> Proof.context) * attribute val section: modifier parser list -> thm list context_parser val sections: modifier parser list -> thm list list context_parser @@ -350,15 +351,12 @@ Name_Space.define context true (binding, (meth, comment)) (Methods.get context); in (name, Context.the_theory (Methods.put meths' context)) end; -fun define binding meth comment lthy = - let val meth0 = meth o Args.transform_values (Local_Theory.background_morphism lthy) in - lthy - |> Local_Theory.background_theory_result (define_global binding meth0 comment) - |-> (fn name => - Local_Theory.map_contexts (K transfer_methods) - #> Local_Theory.generic_alias Methods.map binding name - #> pair name) - end; +fun define binding meth comment = + Local_Theory.background_theory_result (define_global binding meth comment) + #-> (fn name => + Local_Theory.map_contexts (K transfer_methods) + #> Local_Theory.generic_alias Methods.map binding name + #> pair name); (* check *) @@ -393,12 +391,13 @@ fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd; fun method_setup name source cmt = - Context.theory_map (ML_Context.expression (#pos source) + (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ + ML_Lex.read_source false source @ + ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) + |> ML_Context.expression (#pos source) "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" - "Context.map_theory (Method.setup name scan comment)" - (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read_source false source @ - ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))); + "Context.map_proof (Method.local_setup name scan comment)" + |> Context.proof_map;