added none: 'a -> 'a * 'b attribute list;
authorwenzelm
Wed Apr 29 11:24:58 1998 +0200 (1998-04-29)
changeset 4850050481f41e28
parent 4849 a9d5b8f8e40f
child 4851 cbbc53963aaa
added none: 'a -> 'a * 'b attribute list;
added no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list;
added no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list;
added applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list);
src/Pure/attribute.ML
     1.1 --- a/src/Pure/attribute.ML	Wed Apr 29 11:22:52 1998 +0200
     1.2 +++ b/src/Pure/attribute.ML	Wed Apr 29 11:24:58 1998 +0200
     1.3 @@ -18,8 +18,12 @@
     1.4    include BASIC_ATTRIBUTE
     1.5    val thm_of: tthm -> thm
     1.6    val tthm_of: thm -> tthm
     1.7 +  val none: 'a -> 'a * 'b attribute list
     1.8 +  val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
     1.9 +  val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
    1.10    val fail: string -> string -> 'a
    1.11    val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
    1.12 +  val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
    1.13    val pretty_tthm: tthm -> Pretty.T
    1.14    val tag: tag -> 'a attribute
    1.15    val untag: tag -> 'a attribute
    1.16 @@ -47,6 +51,10 @@
    1.17  fun thm_of (thm, _) = thm;
    1.18  fun tthm_of thm = (thm, []);
    1.19  
    1.20 +fun none x = (x, []);
    1.21 +fun no_attrs (x, y) = ((x, (y, [])), []);
    1.22 +fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
    1.23 +
    1.24  
    1.25  (* apply attributes *)
    1.26  
    1.27 @@ -57,8 +65,15 @@
    1.28  fun warn_failed (name, msg) =
    1.29    warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
    1.30  
    1.31 -fun apply (x, []) = x
    1.32 -  | apply (x, f :: fs) = apply (f x handle FAIL info => (warn_failed info; x), fs);
    1.33 +fun apply (x_th, []) = x_th
    1.34 +  | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
    1.35 +
    1.36 +fun applys ((x, []), _) = (x, [])
    1.37 +  | applys ((x, th :: ths), atts) =
    1.38 +      let
    1.39 +        val (x', th') = apply ((x, th), atts);
    1.40 +        val (x'', ths') = applys ((x', ths), atts);
    1.41 +      in (x'', th' :: ths') end;
    1.42  
    1.43  
    1.44  (* display tagged theorems *)
    1.45 @@ -134,7 +149,7 @@
    1.46  
    1.47  (* get global / local attributes *)
    1.48  
    1.49 -fun attrs which thy (raw_name, args) =
    1.50 +fun gen_attr which thy (raw_name, args) =
    1.51    let
    1.52      val {space, attrs} = get_attributes thy;
    1.53      val name = NameSpace.intern space raw_name;
    1.54 @@ -144,8 +159,8 @@
    1.55      | Some p => which p args)
    1.56    end;
    1.57  
    1.58 -val global_attr = attrs fst;
    1.59 -val local_attr = attrs snd;
    1.60 +val global_attr = gen_attr fst;
    1.61 +val local_attr = gen_attr snd;
    1.62  
    1.63  
    1.64  (* add_attrs *)