name_thm etc.: pass position;
authorwenzelm
Tue Sep 02 14:10:25 2008 +0200 (2008-09-02)
changeset 28076b2374a203b1c
parent 28075 a45ce1bae4e0
child 28077 d6102a4fcfce
name_thm etc.: pass position;
note_thms etc.: Name.binding, report fact_decl;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Tue Sep 02 14:10:24 2008 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Sep 02 14:10:25 2008 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4    val burrow_facts: ('a list -> 'b list) ->
     1.5      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
     1.6    val name_multi: string -> 'a list -> (string * 'a) list
     1.7 -  val name_thm: bool -> bool -> string -> thm -> thm
     1.8 -  val name_thms: bool -> bool -> string -> thm list -> thm list
     1.9 -  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
    1.10 +  val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
    1.11 +  val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
    1.12 +  val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
    1.13    val store_thms: bstring * thm list -> theory -> thm list * theory
    1.14    val store_thm: bstring * thm -> theory -> thm * theory
    1.15    val store_thm_open: bstring * thm -> theory -> thm * theory
    1.16 @@ -30,10 +30,10 @@
    1.17    val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
    1.18    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
    1.19    val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
    1.20 -  val note_thmss: string -> ((bstring * attribute list) *
    1.21 -    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
    1.22 -  val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
    1.23 -    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
    1.24 +  val note_thmss: string -> ((Name.binding * attribute list) *
    1.25 +    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
    1.26 +  val note_thmss_grouped: string -> string -> ((Name.binding * attribute list) *
    1.27 +    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
    1.28    val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
    1.29    val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
    1.30    val add_defs: bool -> ((bstring * term) * attribute list) list ->
    1.31 @@ -115,16 +115,17 @@
    1.32    | name_multi "" xs = map (pair "") xs
    1.33    | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
    1.34  
    1.35 -fun name_thm pre official name thm = thm
    1.36 +fun name_thm pre official pos name thm = thm
    1.37    |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
    1.38    |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name)
    1.39 +  |> Thm.default_position pos
    1.40    |> Thm.default_position (Position.thread_data ());
    1.41  
    1.42 -fun name_thms pre official name xs =
    1.43 -  map (uncurry (name_thm pre official)) (name_multi name xs);
    1.44 +fun name_thms pre official pos name xs =
    1.45 +  map (uncurry (name_thm pre official pos)) (name_multi name xs);
    1.46  
    1.47 -fun name_thmss official name fact =
    1.48 -  burrow_fact (name_thms true official name) fact;
    1.49 +fun name_thmss official pos name fact =
    1.50 +  burrow_fact (name_thms true official pos name) fact;
    1.51  
    1.52  
    1.53  (* enter_thms *)
    1.54 @@ -142,17 +143,20 @@
    1.55  
    1.56  (* store_thm(s) *)
    1.57  
    1.58 -val store_thms = enter_thms (name_thms true true) (name_thms false true) I;
    1.59 +val store_thms =
    1.60 +  enter_thms (name_thms true true Position.none) (name_thms false true Position.none) I;
    1.61 +
    1.62  fun store_thm (name, th) = store_thms (name, [th]) #>> the_single;
    1.63  
    1.64  fun store_thm_open (name, th) =
    1.65 -  enter_thms (name_thms true false) (name_thms false false) I (name, [th]) #>> the_single;
    1.66 +  enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
    1.67 +    (name, [th]) #>> the_single;
    1.68  
    1.69  
    1.70  (* add_thms(s) *)
    1.71  
    1.72  fun add_thms_atts pre_name ((bname, thms), atts) =
    1.73 -  enter_thms pre_name (name_thms false true)
    1.74 +  enter_thms pre_name (name_thms false true Position.none)
    1.75      (foldl_map (Thm.theory_attributes atts)) (bname, thms);
    1.76  
    1.77  fun gen_add_thmss pre_name =
    1.78 @@ -161,8 +165,8 @@
    1.79  fun gen_add_thms pre_name args =
    1.80    apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
    1.81  
    1.82 -val add_thmss = gen_add_thmss (name_thms true true);
    1.83 -val add_thms = gen_add_thms (name_thms true true);
    1.84 +val add_thmss = gen_add_thmss (name_thms true true Position.none);
    1.85 +val add_thms = gen_add_thms (name_thms true true Position.none);
    1.86  val add_thm = yield_singleton add_thms;
    1.87  
    1.88  
    1.89 @@ -177,13 +181,18 @@
    1.90  
    1.91  local
    1.92  
    1.93 -fun gen_note_thmss tag = fold_map (fn ((bname, more_atts), ths_atts) => fn thy =>
    1.94 +fun gen_note_thmss tag = fold_map (fn ((binding, more_atts), ths_atts) => fn thy =>
    1.95    let
    1.96 +    val bname = Name.name_of binding;
    1.97 +    val pos = Name.pos_of binding;
    1.98 +    val name = Sign.full_name thy bname;
    1.99 +    val _ = Position.report (Markup.fact_decl name) pos;
   1.100 +
   1.101      fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
   1.102      val (thms, thy') = thy |> enter_thms
   1.103 -      (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app)
   1.104 +      (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app)
   1.105        (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
   1.106 -  in ((bname, thms), thy') end);
   1.107 +  in ((name, thms), thy') end);
   1.108  
   1.109  in
   1.110