src/Pure/Isar/attrib.ML
changeset 8633 427ead639d8a
parent 8496 7e4a466b18d5
child 8687 24bff69370f0
equal deleted inserted replaced
8632:14a69a0e8679 8633:427ead639d8a
    30   val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list)
    30   val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list)
    31   val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    31   val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    32   val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    32   val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    33   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
    33   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
    34   val no_args: 'a attribute -> Args.src -> 'a attribute
    34   val no_args: 'a attribute -> Args.src -> 'a attribute
       
    35   val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
    35   val setup: (theory -> theory) list
    36   val setup: (theory -> theory) list
    36 end;
    37 end;
    37 
    38 
    38 structure Attrib: ATTRIB =
    39 structure Attrib: ATTRIB =
    39 struct
    40 struct
   159 fun syntax scan src (st, th) =
   160 fun syntax scan src (st, th) =
   160   let val (st', f) = Args.syntax "attribute" scan src st
   161   let val (st', f) = Args.syntax "attribute" scan src st
   161   in f (st', th) end;
   162   in f (st', th) end;
   162 
   163 
   163 fun no_args x = syntax (Scan.succeed x);
   164 fun no_args x = syntax (Scan.succeed x);
       
   165 
       
   166 fun add_del_args add del x =
       
   167   syntax (Scan.lift (Args.$$$ "add" >> K add || Args.$$$ "del" >> K del || Scan.succeed add)) x;
   164 
   168 
   165 
   169 
   166 
   170 
   167 (** Pure attributes **)
   171 (** Pure attributes **)
   168 
   172