tuned signature -- prefer Name_Space.get with its builtin error;
authorwenzelm
Mon Mar 10 15:04:01 2014 +0100 (2014-03-10)
changeset 56026893fe12639bc
parent 56025 d74fed45fa8b
child 56027 25889f5c39a8
tuned signature -- prefer Name_Space.get with its builtin error;
src/HOL/Tools/Lifting/lifting_setup.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/method.ML
src/Pure/Isar/specification.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 13:55:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 15:04:01 2014 +0100
     1.3 @@ -954,8 +954,7 @@
     1.4  
     1.5  fun pointer_of_bundle_name bundle_name ctxt =
     1.6    let
     1.7 -    val bundle_name = Bundle.check ctxt bundle_name
     1.8 -    val bundle = Bundle.the_bundle ctxt bundle_name
     1.9 +    val bundle = Bundle.get_bundle_cmd ctxt bundle_name
    1.10    in
    1.11      case bundle of
    1.12        [(_, [arg_src])] => 
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 13:55:03 2014 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 15:04:01 2014 +0100
     2.3 @@ -142,11 +142,10 @@
     2.4  fun attribute_generic context =
     2.5    let val table = get_attributes context in
     2.6      fn src =>
     2.7 -      let val ((name, _), pos) = Args.dest_src src in
     2.8 -        (case Name_Space.lookup_key table name of
     2.9 -          NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
    2.10 -        | SOME (_, (att, _)) => att src)
    2.11 -      end
    2.12 +      let
    2.13 +        val ((name, _), _) = Args.dest_src src;
    2.14 +        val (att, _) = Name_Space.get table name;
    2.15 +      in att src end
    2.16    end;
    2.17  
    2.18  val attribute = attribute_generic o Context.Proof;
     3.1 --- a/src/Pure/Isar/bundle.ML	Mon Mar 10 13:55:03 2014 +0100
     3.2 +++ b/src/Pure/Isar/bundle.ML	Mon Mar 10 15:04:01 2014 +0100
     3.3 @@ -7,8 +7,9 @@
     3.4  signature BUNDLE =
     3.5  sig
     3.6    type bundle = (thm list * Args.src list) list
     3.7 -  val the_bundle: Proof.context -> string -> bundle
     3.8    val check: Proof.context -> xstring * Position.T -> string
     3.9 +  val get_bundle: Proof.context -> string -> bundle
    3.10 +  val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
    3.11    val bundle: binding * (thm list * Args.src list) list ->
    3.12      (binding * typ option * mixfix) list -> local_theory -> local_theory
    3.13    val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
    3.14 @@ -45,12 +46,10 @@
    3.15  
    3.16  val get_bundles = Data.get o Context.Proof;
    3.17  
    3.18 -fun the_bundle ctxt name =
    3.19 -  (case Name_Space.lookup_key (get_bundles ctxt) name of
    3.20 -    SOME (_, bundle) => bundle
    3.21 -  | NONE => error ("Unknown bundle " ^ quote name));
    3.22 +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
    3.23  
    3.24 -fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
    3.25 +val get_bundle = Name_Space.get o get_bundles;
    3.26 +fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
    3.27  
    3.28  
    3.29  (* define bundle *)
    3.30 @@ -85,17 +84,17 @@
    3.31  
    3.32  local
    3.33  
    3.34 -fun gen_includes prep args ctxt =
    3.35 -  let val decls = maps (the_bundle ctxt o prep ctxt) args
    3.36 +fun gen_includes get args ctxt =
    3.37 +  let val decls = maps (get ctxt) args
    3.38    in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
    3.39  
    3.40 -fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
    3.41 +fun gen_context get prep_decl raw_incls raw_elems gthy =
    3.42    let
    3.43      val (after_close, lthy) =
    3.44        gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
    3.45          (pair I o Local_Theory.assert);
    3.46      val ((_, _, _, lthy'), _) = lthy
    3.47 -      |> gen_includes prep_bundle raw_incls
    3.48 +      |> gen_includes get raw_incls
    3.49        |> prep_decl ([], []) I raw_elems;
    3.50    in
    3.51      lthy' |> Local_Theory.open_target
    3.52 @@ -104,8 +103,8 @@
    3.53  
    3.54  in
    3.55  
    3.56 -val includes = gen_includes (K I);
    3.57 -val includes_cmd = gen_includes check;
    3.58 +val includes = gen_includes get_bundle;
    3.59 +val includes_cmd = gen_includes get_bundle_cmd;
    3.60  
    3.61  fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
    3.62  fun include_cmd bs =
    3.63 @@ -114,8 +113,8 @@
    3.64  fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
    3.65  fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
    3.66  
    3.67 -val context = gen_context (K I) Expression.cert_declaration;
    3.68 -val context_cmd = gen_context check Expression.read_declaration;
    3.69 +val context = gen_context get_bundle Expression.cert_declaration;
    3.70 +val context_cmd = gen_context get_bundle_cmd Expression.read_declaration;
    3.71  
    3.72  end;
    3.73  
     4.1 --- a/src/Pure/Isar/method.ML	Mon Mar 10 13:55:03 2014 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 10 15:04:01 2014 +0100
     4.3 @@ -353,11 +353,10 @@
     4.4  fun method ctxt =
     4.5    let val table = get_methods ctxt in
     4.6      fn src =>
     4.7 -      let val ((name, _), pos) = Args.dest_src src in
     4.8 -        (case Name_Space.lookup_key table name of
     4.9 -          NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
    4.10 -        | SOME (_, (meth, _)) => meth src)
    4.11 -      end
    4.12 +      let
    4.13 +        val ((name, _), _) = Args.dest_src src;
    4.14 +        val (meth, _) = Name_Space.get table name;
    4.15 +      in meth src end
    4.16    end;
    4.17  
    4.18  fun method_cmd ctxt = method ctxt o check_src ctxt;
     5.1 --- a/src/Pure/Isar/specification.ML	Mon Mar 10 13:55:03 2014 +0100
     5.2 +++ b/src/Pure/Isar/specification.ML	Mon Mar 10 15:04:01 2014 +0100
     5.3 @@ -376,14 +376,14 @@
     5.4    fun merge data : T = Library.merge (eq_snd op =) data;
     5.5  );
     5.6  
     5.7 -fun gen_theorem schematic prep_bundle prep_att prep_stmt
     5.8 +fun gen_theorem schematic bundle_includes prep_att prep_stmt
     5.9      kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
    5.10    let
    5.11      val _ = Local_Theory.assert lthy;
    5.12  
    5.13      val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
    5.14      val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
    5.15 -      |> Bundle.includes (map (prep_bundle lthy) raw_includes)
    5.16 +      |> bundle_includes raw_includes
    5.17        |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
    5.18      val atts = more_atts @ map (prep_att lthy) raw_atts;
    5.19  
    5.20 @@ -419,13 +419,15 @@
    5.21  
    5.22  in
    5.23  
    5.24 -val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
    5.25 +val theorem =
    5.26 +  gen_theorem false Bundle.includes (K I) Expression.cert_statement;
    5.27  val theorem_cmd =
    5.28 -  gen_theorem false Bundle.check Attrib.check_src Expression.read_statement;
    5.29 +  gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement;
    5.30  
    5.31 -val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
    5.32 +val schematic_theorem =
    5.33 +  gen_theorem true Bundle.includes (K I) Expression.cert_statement;
    5.34  val schematic_theorem_cmd =
    5.35 -  gen_theorem true Bundle.check Attrib.check_src Expression.read_statement;
    5.36 +  gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
    5.37  
    5.38  fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
    5.39  
     6.1 --- a/src/Pure/sign.ML	Mon Mar 10 13:55:03 2014 +0100
     6.2 +++ b/src/Pure/sign.ML	Mon Mar 10 15:04:01 2014 +0100
     6.3 @@ -192,7 +192,7 @@
     6.4  
     6.5  fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
     6.6  
     6.7 -val declared_tyname = is_some oo (Name_Space.lookup_key o #types o Type.rep_tsig o tsig_of);
     6.8 +fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none);
     6.9  val declared_const = can o the_const_constraint;
    6.10  
    6.11