modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
authorwenzelm
Sat Mar 08 21:08:10 2014 +0100 (2014-03-08)
changeset 559979dc5ce83202c
parent 55996 13a7d9661ffc
child 55998 f5f9fad3321c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;
src/Doc/antiquote_setup.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_thms.ML
src/Tools/permanent_interpretation.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Mar 08 13:49:01 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sat Mar 08 21:08:10 2014 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
     1.5    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
     1.6    entity_antiqs (can o Method.check_name) "" "method" #>
     1.7 -  entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
     1.8 +  entity_antiqs (can o Attrib.check_name) "" "attribute" #>
     1.9    entity_antiqs no_check "" "fact" #>
    1.10    entity_antiqs no_check "" "variable" #>
    1.11    entity_antiqs no_check "" "case" #>
     2.1 --- a/src/HOL/Library/simps_case_conv.ML	Sat Mar 08 13:49:01 2014 +0100
     2.2 +++ b/src/HOL/Library/simps_case_conv.ML	Sat Mar 08 21:08:10 2014 +0100
     2.3 @@ -202,8 +202,7 @@
     2.4  
     2.5  fun case_of_simps_cmd (bind, thms_ref) lthy =
     2.6    let
     2.7 -    val thy = Proof_Context.theory_of lthy
     2.8 -    val bind' = apsnd (map (Attrib.intern_src thy)) bind
     2.9 +    val bind' = apsnd (map (Attrib.check_src lthy)) bind
    2.10      val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
    2.11    in
    2.12      Local_Theory.note (bind', [thm]) lthy |> snd
    2.13 @@ -211,8 +210,7 @@
    2.14  
    2.15  fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
    2.16    let
    2.17 -    val thy = Proof_Context.theory_of lthy
    2.18 -    val bind' = apsnd (map (Attrib.intern_src thy)) bind
    2.19 +    val bind' = apsnd (map (Attrib.check_src lthy)) bind
    2.20      val thm = singleton (Attrib.eval_thms lthy) thm_ref
    2.21      val simps = if null splits_ref
    2.22        then to_simps lthy thm
     3.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Sat Mar 08 13:49:01 2014 +0100
     3.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Sat Mar 08 21:08:10 2014 +0100
     3.3 @@ -43,17 +43,16 @@
     3.4  
     3.5  fun gen_fun_cases prep_att prep_prop args lthy =
     3.6    let
     3.7 -    val thy = Proof_Context.theory_of lthy;
     3.8      val thmss =
     3.9        map snd args
    3.10        |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
    3.11      val facts =
    3.12 -      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    3.13 +      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
    3.14          args thmss;
    3.15    in lthy |> Local_Theory.notes facts end;
    3.16  
    3.17  val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
    3.18 -val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
    3.19 +val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
    3.20  
    3.21  val _ =
    3.22    Outer_Syntax.local_theory @{command_spec "fun_cases"}
     4.1 --- a/src/HOL/Tools/inductive.ML	Sat Mar 08 13:49:01 2014 +0100
     4.2 +++ b/src/HOL/Tools/inductive.ML	Sat Mar 08 21:08:10 2014 +0100
     4.3 @@ -576,16 +576,15 @@
     4.4  
     4.5  fun gen_inductive_cases prep_att prep_prop args lthy =
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of lthy;
     4.8      val thmss =
     4.9        map snd args
    4.10        |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
    4.11      val facts =
    4.12 -      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    4.13 +      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
    4.14          args thmss;
    4.15    in lthy |> Local_Theory.notes facts end;
    4.16  
    4.17 -val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    4.18 +val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
    4.19  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    4.20  
    4.21  
    4.22 @@ -635,13 +634,12 @@
    4.23  
    4.24  fun gen_inductive_simps prep_att prep_prop args lthy =
    4.25    let
    4.26 -    val thy = Proof_Context.theory_of lthy;
    4.27      val facts = args |> map (fn ((a, atts), props) =>
    4.28 -      ((a, map (prep_att thy) atts),
    4.29 +      ((a, map (prep_att lthy) atts),
    4.30          map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
    4.31    in lthy |> Local_Theory.notes facts end;
    4.32  
    4.33 -val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
    4.34 +val inductive_simps = gen_inductive_simps Attrib.check_src Syntax.read_prop;
    4.35  val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
    4.36  
    4.37  
     5.1 --- a/src/HOL/Tools/recdef.ML	Sat Mar 08 13:49:01 2014 +0100
     5.2 +++ b/src/HOL/Tools/recdef.ML	Sat Mar 08 21:08:10 2014 +0100
     5.3 @@ -253,7 +253,7 @@
     5.4    let
     5.5      val thy = Proof_Context.theory_of lthy;
     5.6      val name = prep_name thy raw_name;
     5.7 -    val atts = map (prep_att thy) raw_atts;
     5.8 +    val atts = map (prep_att lthy) raw_atts;
     5.9      val tcs =
    5.10        (case get_recdef thy name of
    5.11          NONE => error ("No recdef definition of constant: " ^ quote name)
    5.12 @@ -268,7 +268,7 @@
    5.13        (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    5.14    end;
    5.15  
    5.16 -val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
    5.17 +val recdef_tc = gen_recdef_tc Attrib.check_src Sign.intern_const;
    5.18  val recdef_tc_i = gen_recdef_tc (K I) (K I);
    5.19  
    5.20  
     6.1 --- a/src/HOL/Tools/try0.ML	Sat Mar 08 13:49:01 2014 +0100
     6.2 +++ b/src/HOL/Tools/try0.ML	Sat Mar 08 21:08:10 2014 +0100
     6.3 @@ -57,8 +57,7 @@
     6.4  
     6.5  fun apply_named_method_on_first_goal ctxt =
     6.6    parse_method
     6.7 -  #> Method.check_source ctxt
     6.8 -  #> Method.the_method ctxt
     6.9 +  #> Method.method_cmd ctxt
    6.10    #> Method.Basic
    6.11    #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m))
    6.12    #> Proof.refine;
     7.1 --- a/src/Pure/Isar/args.ML	Sat Mar 08 13:49:01 2014 +0100
     7.2 +++ b/src/Pure/Isar/args.ML	Sat Mar 08 21:08:10 2014 +0100
     7.3 @@ -61,10 +61,10 @@
     7.4    val goal_spec: ((int -> tactic) -> tactic) context_parser
     7.5    val parse: Token.T list parser
     7.6    val parse1: (string -> bool) -> Token.T list parser
     7.7 -  val attribs: (string -> string) -> src list parser
     7.8 -  val opt_attribs: (string -> string) -> src list parser
     7.9 -  val thm_name: (string -> string) -> string -> (binding * src list) parser
    7.10 -  val opt_thm_name: (string -> string) -> string -> (binding * src list) parser
    7.11 +  val attribs: (xstring * Position.T -> string) -> src list parser
    7.12 +  val opt_attribs: (xstring * Position.T -> string) -> src list parser
    7.13 +  val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
    7.14 +  val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
    7.15    val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    7.16    val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    7.17  end;
    7.18 @@ -261,23 +261,23 @@
    7.19  
    7.20  (* attributes *)
    7.21  
    7.22 -fun attribs intern =
    7.23 +fun attribs check =
    7.24    let
    7.25 -    val attrib_name = internal_text || (symbolic || named)
    7.26 -      >> evaluate Token.Text (intern o Token.content_of);
    7.27 +    fun intern tok = check (Token.content_of tok, Token.pos_of tok);
    7.28 +    val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
    7.29      val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
    7.30    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
    7.31  
    7.32 -fun opt_attribs intern = Scan.optional (attribs intern) [];
    7.33 +fun opt_attribs check = Scan.optional (attribs check) [];
    7.34  
    7.35  
    7.36  (* theorem specifications *)
    7.37  
    7.38 -fun thm_name intern s = binding -- opt_attribs intern --| $$$ s;
    7.39 +fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
    7.40  
    7.41 -fun opt_thm_name intern s =
    7.42 +fun opt_thm_name check_attrib s =
    7.43    Scan.optional
    7.44 -    ((binding -- opt_attribs intern || attribs intern >> pair Binding.empty) --| $$$ s)
    7.45 +    ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
    7.46      (Binding.empty, []);
    7.47  
    7.48  
     8.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 08 13:49:01 2014 +0100
     8.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 08 21:08:10 2014 +0100
     8.3 @@ -10,10 +10,11 @@
     8.4    type binding = binding * src list
     8.5    val empty_binding: binding
     8.6    val is_empty_binding: binding -> bool
     8.7 -  val print_attributes: theory -> unit
     8.8 -  val check: theory -> xstring * Position.T -> string
     8.9 -  val intern: theory -> xstring -> string
    8.10 -  val intern_src: theory -> src -> src
    8.11 +  val print_attributes: Proof.context -> unit
    8.12 +  val check_name_generic: Context.generic -> xstring * Position.T -> string
    8.13 +  val check_src_generic: Context.generic -> src -> src
    8.14 +  val check_name: Proof.context -> xstring * Position.T -> string
    8.15 +  val check_src: Proof.context -> src -> src
    8.16    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    8.17    val attribute: Proof.context -> src -> attribute
    8.18    val attribute_global: theory -> src -> attribute
    8.19 @@ -94,10 +95,11 @@
    8.20    fun merge data : T = Name_Space.merge_tables data;
    8.21  );
    8.22  
    8.23 -fun print_attributes thy =
    8.24 +val get_attributes = Attributes.get o Context.theory_of;
    8.25 +
    8.26 +fun print_attributes ctxt =
    8.27    let
    8.28 -    val ctxt = Proof_Context.init_global thy;
    8.29 -    val attribs = Attributes.get thy;
    8.30 +    val attribs = get_attributes (Context.Proof ctxt);
    8.31      fun prt_attr (name, (_, "")) = Pretty.mark_str name
    8.32        | prt_attr (name, (_, comment)) =
    8.33            Pretty.block
    8.34 @@ -111,18 +113,24 @@
    8.35    |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
    8.36  
    8.37  
    8.38 -(* name space *)
    8.39 +(* check *)
    8.40  
    8.41 -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
    8.42 +fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
    8.43  
    8.44 -val intern = Name_Space.intern o #1 o Attributes.get;
    8.45 -val intern_src = Args.map_name o intern;
    8.46 +fun check_src_generic context src =
    8.47 +  let
    8.48 +    val ((xname, toks), pos) = Args.dest_src src;
    8.49 +    val name = check_name_generic context (xname, pos);
    8.50 +  in Args.src ((name, toks), pos) end;
    8.51  
    8.52 -fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
    8.53 +val check_name = check_name_generic o Context.Proof;
    8.54 +val check_src = check_src_generic o Context.Proof;
    8.55  
    8.56  
    8.57  (* pretty printing *)
    8.58  
    8.59 +fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
    8.60 +
    8.61  fun pretty_attribs _ [] = []
    8.62    | pretty_attribs ctxt srcs =
    8.63        [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
    8.64 @@ -131,23 +139,20 @@
    8.65  (* get attributes *)
    8.66  
    8.67  fun attribute_generic context =
    8.68 -  let
    8.69 -    val thy = Context.theory_of context;
    8.70 -    val (space, tab) = Attributes.get thy;
    8.71 -    fun attr src =
    8.72 +  let val (_, tab) = get_attributes context in
    8.73 +    fn src =>
    8.74        let val ((name, _), pos) = Args.dest_src src in
    8.75          (case Symtab.lookup tab name of
    8.76 -          NONE => error ("Unknown attribute: " ^ quote name ^ Position.here pos)
    8.77 -        | SOME (att, _) =>
    8.78 -            (Context_Position.report_generic context pos (Name_Space.markup space name); att src))
    8.79 -      end;
    8.80 -  in attr end;
    8.81 +          NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
    8.82 +        | SOME (att, _) => att src)
    8.83 +      end
    8.84 +  end;
    8.85  
    8.86  val attribute = attribute_generic o Context.Proof;
    8.87  val attribute_global = attribute_generic o Context.Theory;
    8.88  
    8.89 -fun attribute_cmd ctxt = attribute ctxt o intern_src (Proof_Context.theory_of ctxt);
    8.90 -fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
    8.91 +fun attribute_cmd ctxt = attribute ctxt o check_src ctxt;
    8.92 +fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy);
    8.93  
    8.94  
    8.95  (* attributed declarations *)
    8.96 @@ -221,12 +226,11 @@
    8.97  
    8.98  fun gen_thm pick = Scan.depend (fn context =>
    8.99    let
   8.100 -    val thy = Context.theory_of context;
   8.101      val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
   8.102      val get_fact = get o Facts.Fact;
   8.103      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   8.104    in
   8.105 -    Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
   8.106 +    Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
   8.107        let
   8.108          val atts = map (attribute_generic context) srcs;
   8.109          val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
   8.110 @@ -237,7 +241,7 @@
   8.111       Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
   8.112        Args.named_fact (get_named pos) -- Scan.option thm_sel
   8.113          >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
   8.114 -    -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
   8.115 +    -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
   8.116        let
   8.117          val ths = Facts.select thmref fact;
   8.118          val atts = map (attribute_generic context) srcs;
   8.119 @@ -340,13 +344,13 @@
   8.120  
   8.121  fun print_options ctxt =
   8.122    let
   8.123 -    val thy = Proof_Context.theory_of ctxt;
   8.124      fun prt (name, config) =
   8.125        let val value = Config.get ctxt config in
   8.126          Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
   8.127            Pretty.brk 1, Pretty.str (Config.print_value value)]
   8.128        end;
   8.129 -    val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
   8.130 +    val space = #1 (get_attributes (Context.Proof ctxt));
   8.131 +    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
   8.132    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   8.133  
   8.134  
     9.1 --- a/src/Pure/Isar/bundle.ML	Sat Mar 08 13:49:01 2014 +0100
     9.2 +++ b/src/Pure/Isar/bundle.ML	Sat Mar 08 21:08:10 2014 +0100
     9.3 @@ -76,9 +76,7 @@
     9.4  in
     9.5  
     9.6  val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
     9.7 -val bundle_cmd =
     9.8 -  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
     9.9 -    Proof_Context.read_vars;
    9.10 +val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
    9.11  
    9.12  end;
    9.13  
    10.1 --- a/src/Pure/Isar/element.ML	Sat Mar 08 13:49:01 2014 +0100
    10.2 +++ b/src/Pure/Isar/element.ML	Sat Mar 08 21:08:10 2014 +0100
    10.3 @@ -528,7 +528,7 @@
    10.4      term = I,
    10.5      pattern = I,
    10.6      fact = Proof_Context.get_fact ctxt,
    10.7 -    attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
    10.8 +    attrib = Attrib.check_src ctxt}
    10.9    in activate_i elem ctxt end;
   10.10  
   10.11  end;
    11.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 08 13:49:01 2014 +0100
    11.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 08 21:08:10 2014 +0100
    11.3 @@ -851,8 +851,7 @@
    11.4    let
    11.5      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    11.6      val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    11.7 -    val attrss =
    11.8 -      map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
    11.9 +    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
   11.10      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
   11.11      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   11.12    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
   11.13 @@ -861,7 +860,7 @@
   11.14    prep_interpretation cert_goal_expression (K I) (K I);
   11.15  
   11.16  val read_interpretation =
   11.17 -  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
   11.18 +  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
   11.19  
   11.20  
   11.21  (* generic interpretation machinery *)
    12.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 08 13:49:01 2014 +0100
    12.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 08 21:08:10 2014 +0100
    12.3 @@ -799,7 +799,7 @@
    12.4    Outer_Syntax.improper_command @{command_spec "print_attributes"}
    12.5      "print attributes of this theory"
    12.6      (Scan.succeed (Toplevel.unknown_theory o
    12.7 -      Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
    12.8 +      Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
    12.9  
   12.10  val _ =
   12.11    Outer_Syntax.improper_command @{command_spec "print_simpset"}
    13.1 --- a/src/Pure/Isar/method.ML	Sat Mar 08 13:49:01 2014 +0100
    13.2 +++ b/src/Pure/Isar/method.ML	Sat Mar 08 21:08:10 2014 +0100
    13.3 @@ -63,9 +63,10 @@
    13.4    val sorry_text: bool -> text
    13.5    val finish_text: text option * bool -> text
    13.6    val print_methods: Proof.context -> unit
    13.7 -  val the_method: Proof.context -> src -> Proof.context -> method
    13.8    val check_name: Proof.context -> xstring * Position.T -> string
    13.9 -  val check_source: Proof.context -> src -> src
   13.10 +  val check_src: Proof.context -> src -> src
   13.11 +  val method: Proof.context -> src -> Proof.context -> method
   13.12 +  val method_cmd: Proof.context -> src -> Proof.context -> method
   13.13    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   13.14    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   13.15    val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
   13.16 @@ -335,26 +336,31 @@
   13.17  fun add_method name meth comment thy = thy
   13.18    |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
   13.19  
   13.20 -fun the_method ctxt =
   13.21 +
   13.22 +(* check *)
   13.23 +
   13.24 +fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
   13.25 +
   13.26 +fun check_src ctxt src =
   13.27 +  let
   13.28 +    val ((xname, toks), pos) = Args.dest_src src;
   13.29 +    val name = check_name ctxt (xname, pos);
   13.30 +  in Args.src ((name, toks), pos) end;
   13.31 +
   13.32 +
   13.33 +(* get methods *)
   13.34 +
   13.35 +fun method ctxt =
   13.36    let val (_, tab) = get_methods ctxt in
   13.37      fn src =>
   13.38        let val ((name, _), pos) = Args.dest_src src in
   13.39          (case Symtab.lookup tab name of
   13.40            NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
   13.41 -        | SOME (method, _) => method src)
   13.42 +        | SOME (meth, _) => meth src)
   13.43        end
   13.44    end;
   13.45  
   13.46 -
   13.47 -(* check *)
   13.48 -
   13.49 -fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
   13.50 -
   13.51 -fun check_source ctxt src =
   13.52 -  let
   13.53 -    val ((xname, toks), pos) = Args.dest_src src;
   13.54 -    val name = check_name ctxt (xname, pos);
   13.55 -  in Args.src ((name, toks), pos) end;
   13.56 +fun method_cmd ctxt = method ctxt o check_src ctxt;
   13.57  
   13.58  
   13.59  (* method setup *)
    14.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 08 13:49:01 2014 +0100
    14.2 +++ b/src/Pure/Isar/proof.ML	Sat Mar 08 21:08:10 2014 +0100
    14.3 @@ -421,8 +421,7 @@
    14.4      val ctxt = context_of state;
    14.5  
    14.6      fun eval (Method.Basic m) = apply_method current_context m
    14.7 -      | eval (Method.Source src) =
    14.8 -          apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
    14.9 +      | eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src)
   14.10        | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts)
   14.11        | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts)
   14.12        | eval (Method.Try (_, txt)) = Seq.TRY (eval txt)
    15.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 08 13:49:01 2014 +0100
    15.2 +++ b/src/Pure/Isar/specification.ML	Sat Mar 08 21:08:10 2014 +0100
    15.3 @@ -113,8 +113,6 @@
    15.4  
    15.5  fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
    15.6    let
    15.7 -    val thy = Proof_Context.theory_of ctxt;
    15.8 -
    15.9      val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
   15.10      val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
   15.11  
   15.12 @@ -136,7 +134,7 @@
   15.13  
   15.14      val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
   15.15      val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
   15.16 -    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
   15.17 +    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
   15.18    in ((params, name_atts ~~ specs), specs_ctxt) end;
   15.19  
   15.20  
   15.21 @@ -150,16 +148,16 @@
   15.22  in
   15.23  
   15.24  fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
   15.25 -fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true x;
   15.26 +fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true x;
   15.27  
   15.28  fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
   15.29 -fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src false x;
   15.30 +fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src false x;
   15.31  
   15.32  fun check_specification vars specs =
   15.33    prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
   15.34  
   15.35  fun read_specification vars specs =
   15.36 -  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
   15.37 +  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true vars [specs];
   15.38  
   15.39  end;
   15.40  
   15.41 @@ -293,10 +291,9 @@
   15.42  fun gen_theorems prep_fact prep_att prep_vars
   15.43      kind raw_facts raw_fixes int lthy =
   15.44    let
   15.45 -    val attrib = prep_att (Proof_Context.theory_of lthy);
   15.46      val facts = raw_facts |> map (fn ((name, atts), bs) =>
   15.47 -      ((name, map attrib atts),
   15.48 -        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   15.49 +      ((name, map (prep_att lthy) atts),
   15.50 +        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts))));
   15.51      val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
   15.52  
   15.53      val facts' = facts
   15.54 @@ -309,7 +306,7 @@
   15.55  in
   15.56  
   15.57  val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
   15.58 -val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src Proof_Context.read_vars;
   15.59 +val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
   15.60  
   15.61  end;
   15.62  
   15.63 @@ -384,15 +381,12 @@
   15.64      kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   15.65    let
   15.66      val _ = Local_Theory.assert lthy;
   15.67 -    val thy = Proof_Context.theory_of lthy;
   15.68  
   15.69 -    val attrib = prep_att thy;
   15.70 -
   15.71 -    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
   15.72 +    val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
   15.73      val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
   15.74        |> Bundle.includes (map (prep_bundle lthy) raw_includes)
   15.75 -      |> prep_statement attrib prep_stmt elems raw_concl;
   15.76 -    val atts = more_atts @ map attrib raw_atts;
   15.77 +      |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
   15.78 +    val atts = more_atts @ map (prep_att lthy) raw_atts;
   15.79  
   15.80      fun after_qed' results goal_ctxt' =
   15.81        let
   15.82 @@ -428,11 +422,11 @@
   15.83  
   15.84  val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
   15.85  val theorem_cmd =
   15.86 -  gen_theorem false Bundle.check Attrib.intern_src Expression.read_statement;
   15.87 +  gen_theorem false Bundle.check Attrib.check_src Expression.read_statement;
   15.88  
   15.89  val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
   15.90  val schematic_theorem_cmd =
   15.91 -  gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement;
   15.92 +  gen_theorem true Bundle.check Attrib.check_src Expression.read_statement;
   15.93  
   15.94  fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
   15.95  
    16.1 --- a/src/Pure/ML/ml_thms.ML	Sat Mar 08 13:49:01 2014 +0100
    16.2 +++ b/src/Pure/ML/ml_thms.ML	Sat Mar 08 21:08:10 2014 +0100
    16.3 @@ -39,10 +39,9 @@
    16.4      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
    16.5        let
    16.6          val ctxt = Context.the_proof context;
    16.7 -        val thy = Proof_Context.theory_of ctxt;
    16.8  
    16.9          val i = serial ();
   16.10 -        val srcs = map (Attrib.intern_src thy) raw_srcs;
   16.11 +        val srcs = map (Attrib.check_src ctxt) raw_srcs;
   16.12          val _ = map (Attrib.attribute ctxt) srcs;
   16.13          val (a, ctxt') = ctxt
   16.14            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
    17.1 --- a/src/Tools/permanent_interpretation.ML	Sat Mar 08 13:49:01 2014 +0100
    17.2 +++ b/src/Tools/permanent_interpretation.ML	Sat Mar 08 21:08:10 2014 +0100
    17.3 @@ -41,13 +41,16 @@
    17.4      (*setting up*)
    17.5      val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
    17.6        (*FIXME: only re-prepare if defs are given*)
    17.7 -    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
    17.8 +    val attrss = map (apsnd (map (prep_attr expr_ctxt)) o fst) raw_eqns;
    17.9      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
   17.10      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   17.11    in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
   17.12  
   17.13 -val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
   17.14 -val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
   17.15 +val cert_interpretation =
   17.16 +  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
   17.17 +
   17.18 +val read_interpretation =
   17.19 +  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
   17.20  
   17.21  
   17.22  (* generic interpretation machinery *)