more positions;
authorwenzelm
Tue Feb 25 11:36:04 2014 +0100 (2014-02-25)
changeset 5574011dd48f84441
parent 55739 d8270c17b5be
child 55741 b969263fcf02
more positions;
tuned messages;
src/Pure/Isar/attrib.ML
src/Pure/Isar/proof_context.ML
src/Pure/facts.ML
src/Pure/global_theory.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Feb 25 10:50:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Feb 25 11:36:04 2014 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4        let
     1.5          val atts = map (attribute_generic context) srcs;
     1.6          val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
     1.7 -      in (context', pick "" [th']) end)
     1.8 +      in (context', pick ("", Position.none) [th']) end)
     1.9      ||
    1.10      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.11        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    1.12 @@ -244,7 +244,7 @@
    1.13          val atts = map (attribute_generic context) srcs;
    1.14          val (ths', context') =
    1.15            fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    1.16 -      in (context', pick name ths') end)
    1.17 +      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
    1.18    end);
    1.19  
    1.20  in
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Feb 25 10:50:12 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Feb 25 11:36:04 2014 +0100
     2.3 @@ -933,7 +933,7 @@
     2.4              [res] => res
     2.5            | [] => err "Failed to retrieve literal fact"
     2.6            | _ => err "Ambiguous specification of literal fact");
     2.7 -      in pick "" [res] end
     2.8 +      in pick ("", Position.none) [res] end
     2.9    | retrieve_thms pick ctxt xthmref =
    2.10        let
    2.11          val thy = theory_of ctxt;
    2.12 @@ -950,7 +950,7 @@
    2.13                    (Name_Space.markup (Facts.space_of local_facts) name);
    2.14                   map (Thm.transfer thy) (Facts.select thmref ths))
    2.15              | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
    2.16 -      in pick name thms end;
    2.17 +      in pick (name, pos) thms end;
    2.18  
    2.19  in
    2.20  
     3.1 --- a/src/Pure/facts.ML	Tue Feb 25 10:50:12 2014 +0100
     3.2 +++ b/src/Pure/facts.ML	Tue Feb 25 11:36:04 2014 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  signature FACTS =
     3.6  sig
     3.7 -  val the_single: string -> thm list -> thm
     3.8 +  val the_single: string * Position.T -> thm list -> thm
     3.9    datatype interval = FromTo of int * int | From of int | Single of int
    3.10    datatype ref =
    3.11      Named of (string * Position.T) * interval list option |
    3.12 @@ -46,7 +46,9 @@
    3.13  (** fact references **)
    3.14  
    3.15  fun the_single _ [th] : thm = th
    3.16 -  | the_single name _ = error ("Expected singleton fact " ^ quote name);
    3.17 +  | the_single (name, pos) ths =
    3.18 +      error ("Expected singleton fact " ^ quote name ^
    3.19 +        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
    3.20  
    3.21  
    3.22  (* datatype interval *)
    3.23 @@ -77,12 +79,15 @@
    3.24  
    3.25  fun named name = Named ((name, Position.none), NONE);
    3.26  
    3.27 +fun name_of_ref (Named ((name, _), _)) = name
    3.28 +  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
    3.29 +
    3.30 +fun pos_of_ref (Named ((_, pos), _)) = pos
    3.31 +  | pos_of_ref (Fact _) = Position.none;
    3.32 +
    3.33  fun name_pos_of_ref (Named (name_pos, _)) = name_pos
    3.34    | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact";
    3.35  
    3.36 -val name_of_ref = #1 o name_pos_of_ref;
    3.37 -val pos_of_ref = #2 o name_pos_of_ref;
    3.38 -
    3.39  fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    3.40    | map_name_of_ref _ r = r;
    3.41  
    3.42 @@ -101,7 +106,7 @@
    3.43        let
    3.44          val n = length ths;
    3.45          fun err msg =
    3.46 -          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    3.47 +          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    3.48              Position.here pos);
    3.49          fun sel i =
    3.50            if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
     4.1 --- a/src/Pure/global_theory.ML	Tue Feb 25 10:50:12 2014 +0100
     4.2 +++ b/src/Pure/global_theory.ML	Tue Feb 25 11:36:04 2014 +0100
     4.3 @@ -86,7 +86,7 @@
     4.4    end;
     4.5  
     4.6  fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
     4.7 -fun get_thm thy name = Facts.the_single name (get_thms thy name);
     4.8 +fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
     4.9  
    4.10  fun all_thms_of thy =
    4.11    Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
     5.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 10:50:12 2014 +0100
     5.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 11:36:04 2014 +0100
     5.3 @@ -166,8 +166,8 @@
     5.4  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
     5.5    let
     5.6      val ctxt = Proof_Context.init_global thy;
     5.7 -    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
     5.8 -    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
     5.9 +    val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
    5.10 +    val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
    5.11      val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
    5.12      val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
    5.13    in rep_datatype_i elim induct case_eqns recursor_eqns thy end;