1.1 --- a/NEWS	Sat Nov 19 17:20:17 2011 +0100
     1.2 +++ b/NEWS	Sat Nov 19 21:18:38 2011 +0100
     1.3 @@ -137,6 +137,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Antiquotation @{attributes [...]} embeds attribute source
     1.8 +representation into the ML text, which is particularly useful with
     1.9 +declarations like Local_Theory.note.
    1.10 +
    1.11  * Structure Proof_Context follows standard naming scheme.  Old
    1.12  ProofContext has been discontinued.  INCOMPATIBILITY.
    1.13  

     2.1 --- a/doc-src/IsarImplementation/Thy/Isar.thy	Sat Nov 19 17:20:17 2011 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/Isar.thy	Sat Nov 19 21:18:38 2011 +0100
     2.3 @@ -562,6 +562,27 @@
     2.4    \end{description}
     2.5  *}
     2.6  
     2.7 +text %mlantiq {*
     2.8 +  \begin{matharray}{rcl}
     2.9 +  @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\
    2.10 +  \end{matharray}
    2.11 +
    2.12 +  @{rail "
    2.13 +  @@{ML_antiquotation attributes} attributes
    2.14 +  "}
    2.15 +
    2.16 +  \begin{description}
    2.17 +
    2.18 +  \item @{text "@{attributes [\<dots>]}"} embeds attribute source
    2.19 +  representation into the ML text, which is particularly useful with
    2.20 +  declarations like @{ML Local_Theory.note}.  Attribute names are
    2.21 +  internalized at compile time, but the source is unevaluated.  This
    2.22 +  means attributes with formal arguments (types, terms, theorems) may
    2.23 +  be subject to odd effects of dynamic scoping!
    2.24 +
    2.25 +  \end{description}
    2.26 +*}
    2.27 +
    2.28  text %mlex {* See also @{command attribute_setup} in
    2.29    \cite{isabelle-isar-ref} which includes some abstract examples. *}
    2.30  

     3.1 --- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Sat Nov 19 17:20:17 2011 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Sat Nov 19 21:18:38 2011 +0100
     3.3 @@ -900,6 +900,45 @@
     3.4  %
     3.5  \endisadelimmlref
     3.6  %
     3.7 +\isadelimmlantiq
     3.8 +%
     3.9 +\endisadelimmlantiq
    3.10 +%
    3.11 +\isatagmlantiq
    3.12 +%
    3.13 +\begin{isamarkuptext}%
    3.14 +\begin{matharray}{rcl}
    3.15 +  \indexdef{}{ML antiquotation}{attributes}\hypertarget{ML antiquotation.attributes}{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
    3.16 +  \end{matharray}
    3.17 +
    3.18 +  \begin{railoutput}
    3.19 +\rail@begin{1}{}
    3.20 +\rail@term{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}}[]
    3.21 +\rail@nont{\isa{attributes}}[]
    3.22 +\rail@end
    3.23 +\end{railoutput}
    3.24 +
    3.25 +
    3.26 +  \begin{description}
    3.27 +
    3.28 +  \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}attributes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}} embeds attribute source
    3.29 +  representation into the ML text, which is particularly useful with
    3.30 +  declarations like \verb|Local_Theory.note|.  Attribute names are
    3.31 +  internalized at compile time, but the source is unevaluated.  This
    3.32 +  means attributes with formal arguments (types, terms, theorems) may
    3.33 +  be subject to odd effects of dynamic scoping!
    3.34 +
    3.35 +  \end{description}%
    3.36 +\end{isamarkuptext}%
    3.37 +\isamarkuptrue%
    3.38 +%
    3.39 +\endisatagmlantiq
    3.40 +{\isafoldmlantiq}%
    3.41 +%
    3.42 +\isadelimmlantiq
    3.43 +%
    3.44 +\endisadelimmlantiq
    3.45 +%
    3.46  \isadelimmlex
    3.47  %
    3.48  \endisadelimmlex

     4.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Nov 19 17:20:17 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Nov 19 21:18:38 2011 +0100
     4.3 @@ -363,8 +363,7 @@
     4.4      val simps : (Attrib.binding * thm) list list =
     4.5        map (make_simps lthy) (unfold_thms ~~ blocks')
     4.6      fun mk_bind n : Attrib.binding =
     4.7 -     (Binding.qualify true n (Binding.name "simps"),
     4.8 -       [Attrib.internal (K Simplifier.simp_add)])
     4.9 +     (Binding.qualify true n (Binding.name "simps"), @{attributes [simp]})
    4.10      val simps1 : (Attrib.binding * thm list) list =
    4.11        map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps)
    4.12      val simps2 : (Attrib.binding * thm list) list =

     5.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Nov 19 17:20:17 2011 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Nov 19 21:18:38 2011 +0100
     5.3 @@ -364,17 +364,16 @@
     5.4      Variable.add_fixes (map fst lsrs) |> snd |>
     5.5      Proof.theorem NONE
     5.6        (fn thss => fn goal_ctxt =>
     5.7 -         let
     5.8 -           val simps = Proof_Context.export goal_ctxt lthy' (flat thss);
     5.9 -           val (simps', lthy'') =
    5.10 +        let
    5.11 +          val simps = Proof_Context.export goal_ctxt lthy' (flat thss);
    5.12 +          val (simps', lthy'') =
    5.13              fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy';
    5.14 -         in
    5.15 -           lthy''
    5.16 -           |> Local_Theory.note ((qualify (Binding.name "simps"),
    5.17 -                map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    5.18 -                maps snd simps')
    5.19 -           |> snd
    5.20 -         end)
    5.21 +        in
    5.22 +          lthy''
    5.23 +          |> Local_Theory.note
    5.24 +            ((qualify (Binding.name "simps"), @{attributes [simp, nitpick_simp]}), maps snd simps')
    5.25 +          |> snd
    5.26 +        end)
    5.27        [goals] |>
    5.28      Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
    5.29        rewrite_goals_tac defs_thms THEN

     6.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 17:20:17 2011 +0100
     6.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 21:18:38 2011 +0100
     6.3 @@ -260,21 +260,18 @@
     6.4           (Const (@{const_name last_el}, T), List.last cs)))
     6.5        (fn _ => simp_tac (simpset_of lthy' addsimps
     6.6           [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
     6.7 -
     6.8 -    val simp_att = [Attrib.internal (K Simplifier.simp_add)]
     6.9 -
    6.10    in
    6.11      lthy' |>
    6.12      Local_Theory.note
    6.13 -      ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>
    6.14 +      ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>
    6.15      Local_Theory.note
    6.16 -      ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
    6.17 +      ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>
    6.18      Local_Theory.note
    6.19 -      ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
    6.20 +      ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>
    6.21      Local_Theory.note
    6.22 -      ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
    6.23 +      ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>
    6.24      Local_Theory.note
    6.25 -      ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
    6.26 +      ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>
    6.27      Local_Theory.exit_global
    6.28    end;
    6.29  

     7.1 --- a/src/HOL/Tools/Function/function.ML	Sat Nov 19 17:20:17 2011 +0100
     7.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Nov 19 21:18:38 2011 +0100
     7.3 @@ -45,13 +45,11 @@
     7.4  open Function_Lib
     7.5  open Function_Common
     7.6  
     7.7 -val simp_attribs = map (Attrib.internal o K)
     7.8 -  [Simplifier.simp_add,
     7.9 -   Code.add_default_eqn_attribute,
    7.10 -   Nitpick_Simps.add]
    7.11 +val simp_attribs =
    7.12 +  @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)]
    7.13  
    7.14 -val psimp_attribs = map (Attrib.internal o K)
    7.15 -  [Nitpick_Psimps.add]
    7.16 +val psimp_attribs =
    7.17 +  @{attributes [nitpick_psimp]}
    7.18  
    7.19  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    7.20  

     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Nov 19 17:20:17 2011 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Nov 19 21:18:38 2011 +0100
     8.3 @@ -1419,6 +1419,7 @@
     8.4      val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
     8.5        (maps_modes result_thms)
     8.6      val qname = #qname (dest_steps steps)
     8.7 +    (* FIXME !? *)
     8.8      val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
     8.9        (fn thm => Context.mapping (Code.add_eqn thm) I))))
    8.10      val thy''' =

     9.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Nov 19 17:20:17 2011 +0100
     9.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Nov 19 21:18:38 2011 +0100
     9.3 @@ -325,10 +325,11 @@
     9.4            (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
     9.5        in
     9.6          fold (fn (name, eq) => Local_Theory.note
     9.7 -        ((Binding.conceal (Binding.qualify true prfx
     9.8 -           (Binding.qualify true name (Binding.name "simps"))),
     9.9 -           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    9.10 -             [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy
    9.11 +          ((Binding.conceal
    9.12 +            (Binding.qualify true prfx
    9.13 +              (Binding.qualify true name (Binding.name "simps"))),
    9.14 +             Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd)
    9.15 +          (names ~~ eqs) lthy
    9.16        end)
    9.17  
    9.18  (** ensuring sort constraints **)

    10.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Nov 19 17:20:17 2011 +0100
    10.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Nov 19 21:18:38 2011 +0100
    10.3 @@ -171,8 +171,7 @@
    10.4      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
    10.5      |-> (fn proto_simps => prove_simps proto_simps)
    10.6      |-> (fn simps => Local_Theory.note
    10.7 -      ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    10.8 -          [Simplifier.simp_add, Nitpick_Simps.add]), simps))
    10.9 +      ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
   10.10      |> snd
   10.11    end
   10.12  

    11.1 --- a/src/HOL/Tools/choice_specification.ML	Sat Nov 19 17:20:17 2011 +0100
    11.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Nov 19 21:18:38 2011 +0100
    11.3 @@ -194,8 +194,9 @@
    11.4                          args |> apsnd (remove_alls frees)
    11.5                               |> apsnd undo_imps
    11.6                               |> apsnd Drule.export_without_context
    11.7 -                             |> Thm.theory_attributes (map (Attrib.attribute thy)
    11.8 -                                                           (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts))
    11.9 +                             |> Thm.theory_attributes
   11.10 +                                (map (Attrib.attribute thy)
   11.11 +                                  (@{attributes [nitpick_choice_spec]} @ atts))
   11.12                               |> add_final
   11.13                               |> Library.swap
   11.14                      end

    12.1 --- a/src/HOL/Tools/inductive.ML	Sat Nov 19 17:20:17 2011 +0100
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sat Nov 19 21:18:38 2011 +0100
    12.3 @@ -775,9 +775,9 @@
    12.4        |> Local_Theory.conceal
    12.5        |> Local_Theory.define
    12.6          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    12.7 -         ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]),
    12.8 -         fold_rev lambda params
    12.9 -           (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   12.10 +         ((Binding.empty, @{attributes [nitpick_unfold]}),
   12.11 +           fold_rev lambda params
   12.12 +             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   12.13        ||> Local_Theory.restore_naming lthy;
   12.14      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
   12.15        (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));

    13.1 --- a/src/HOL/Tools/primrec.ML	Sat Nov 19 17:20:17 2011 +0100
    13.2 +++ b/src/HOL/Tools/primrec.ML	Sat Nov 19 21:18:38 2011 +0100
    13.3 @@ -276,8 +276,7 @@
    13.4      fun attr_bindings prefix = map (fn ((b, attrs), _) =>
    13.5        (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
    13.6      fun simp_attr_binding prefix =
    13.7 -      (Binding.qualify true prefix (Binding.name "simps"),
    13.8 -        map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
    13.9 +      (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   13.10    in
   13.11      lthy
   13.12      |> add_primrec_simple fixes (map snd spec)

    14.1 --- a/src/Pure/Isar/parse_spec.ML	Sat Nov 19 17:20:17 2011 +0100
    14.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat Nov 19 21:18:38 2011 +0100
    14.3 @@ -6,7 +6,6 @@
    14.4  
    14.5  signature PARSE_SPEC =
    14.6  sig
    14.7 -  val attrib: Attrib.src parser
    14.8    val attribs: Attrib.src list parser
    14.9    val opt_attribs: Attrib.src list parser
   14.10    val thm_name: string -> Attrib.binding parser

    15.1 --- a/src/Pure/ML/ml_thms.ML	Sat Nov 19 17:20:17 2011 +0100
    15.2 +++ b/src/Pure/ML/ml_thms.ML	Sat Nov 19 21:18:38 2011 +0100
    15.3 @@ -1,11 +1,12 @@
    15.4  (*  Title:      Pure/ML/ml_thms.ML
    15.5      Author:     Makarius
    15.6  
    15.7 -Isar theorem values within ML.
    15.8 +Attribute source and theorem values within ML.
    15.9  *)
   15.10  
   15.11  signature ML_THMS =
   15.12  sig
   15.13 +  val the_attributes: Proof.context -> int -> Args.src list
   15.14    val the_thms: Proof.context -> int -> thm list
   15.15    val the_thm: Proof.context -> int -> thm
   15.16  end;
   15.17 @@ -13,26 +14,49 @@
   15.18  structure ML_Thms: ML_THMS =
   15.19  struct
   15.20  
   15.21 -(* auxiliary facts table *)
   15.22 +(* auxiliary data *)
   15.23  
   15.24 -structure Aux_Facts = Proof_Data
   15.25 +structure Data = Proof_Data
   15.26  (
   15.27 -  type T = thm list Inttab.table;
   15.28 -  fun init _ = Inttab.empty;
   15.29 +  type T = Args.src list Inttab.table * thm list Inttab.table;
   15.30 +  fun init _ = (Inttab.empty, Inttab.empty);
   15.31  );
   15.32  
   15.33 -val put_thms = Aux_Facts.map o Inttab.update;
   15.34 +val put_attributes = Data.map o apfst o Inttab.update;
   15.35 +fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
   15.36  
   15.37 -fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
   15.38 +val put_thms = Data.map o apsnd o Inttab.update;
   15.39 +
   15.40 +fun the_thms ctxt name = the (Inttab.lookup (snd (Data.get ctxt)) name);
   15.41  fun the_thm ctxt name = the_single (the_thms ctxt name);
   15.42  
   15.43 +
   15.44 +(* attribute source *)
   15.45 +
   15.46 +val _ =
   15.47 +  Context.>> (Context.map_theory
   15.48 +    (ML_Context.add_antiq (Binding.name "attributes")
   15.49 +      (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background =>
   15.50 +        let
   15.51 +          val thy = Proof_Context.theory_of background;
   15.52 +
   15.53 +          val i = serial ();
   15.54 +          val srcs = map (Attrib.intern_src thy) raw_srcs;
   15.55 +          val _ = map (Attrib.attribute_i thy) srcs;
   15.56 +          val (a, background') = background
   15.57 +            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
   15.58 +          val ml =
   15.59 +            ("val " ^ a ^ " = ML_Thms.the_attributes (ML_Context.the_local_context ()) " ^
   15.60 +              string_of_int i ^ ";\n", "Isabelle." ^ a);
   15.61 +        in (K ml, background') end))));
   15.62 +
   15.63 +
   15.64 +(* fact references *)
   15.65 +
   15.66  fun thm_bind kind a i =
   15.67    "val " ^ a ^ " = ML_Thms.the_" ^ kind ^
   15.68      " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
   15.69  
   15.70 -
   15.71 -(* fact references *)
   15.72 -
   15.73  fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
   15.74    (fn _ => scan >> (fn ths => fn background =>
   15.75      let

    16.1 --- a/src/Pure/ROOT.ML	Sat Nov 19 17:20:17 2011 +0100
    16.2 +++ b/src/Pure/ROOT.ML	Sat Nov 19 21:18:38 2011 +0100
    16.3 @@ -207,7 +207,6 @@
    16.4  use "Isar/skip_proof.ML";
    16.5  use "Isar/method.ML";
    16.6  use "Isar/proof.ML";
    16.7 -use "ML/ml_thms.ML";
    16.8  use "Isar/element.ML";
    16.9  
   16.10  (*derived theory and proof elements*)
   16.11 @@ -235,6 +234,7 @@
   16.12  use "Isar/spec_rules.ML";
   16.13  use "Isar/specification.ML";
   16.14  use "Isar/typedecl.ML";
   16.15 +use "ML/ml_thms.ML";
   16.16  
   16.17  (*toplevel transactions*)
   16.18  use "Isar/proof_node.ML";