added setup and attribute_setup -- expect plain parser instead of syntax function;
authorwenzelm
Sun Mar 15 15:59:43 2009 +0100 (2009-03-15)
changeset 305258a5a0aa30e1c
parent 30524 92af4e8c54a6
child 30526 7f9a9ec1c94d
added setup and attribute_setup -- expect plain parser instead of syntax function;
aded add_del parser;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 15 15:59:43 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 15 15:59:43 2009 +0100
     1.3 @@ -25,7 +25,10 @@
     1.4    val crude_closure: Proof.context -> src -> src
     1.5    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     1.6    val syntax: attribute context_parser -> src -> attribute
     1.7 +  val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     1.8 +  val attribute_setup: string * Position.T -> string * Position.T -> string -> theory -> theory
     1.9    val no_args: attribute -> src -> attribute
    1.10 +  val add_del: attribute -> attribute -> attribute context_parser
    1.11    val add_del_args: attribute -> attribute -> src -> attribute
    1.12    val thm_sel: Facts.interval list parser
    1.13    val thm: thm context_parser
    1.14 @@ -150,16 +153,27 @@
    1.15    in Attributes.map add thy end;
    1.16  
    1.17  
    1.18 -(* attribute syntax *)
    1.19 +(* attribute setup *)
    1.20 +
    1.21 +fun syntax scan src (context, th) =
    1.22 +  let val (f: attribute, context') = Args.syntax "attribute" scan src context
    1.23 +  in f (context', th) end;
    1.24 +
    1.25 +fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
    1.26  
    1.27 -fun syntax scan src (st, th) =
    1.28 -  let val (f: attribute, st') = Args.syntax "attribute" scan src st
    1.29 -  in f (st', th) end;
    1.30 +fun attribute_setup name (txt, pos) cmt =
    1.31 +  Context.theory_map (ML_Context.expression pos
    1.32 +    "val (name, scan, comment): binding * attribute context_parser * string"
    1.33 +    "Context.map_theory (Attrib.setup name scan comment)"
    1.34 +    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
    1.35 +
    1.36 +
    1.37 +(* basic syntax *)
    1.38  
    1.39  fun no_args x = syntax (Scan.succeed x);
    1.40  
    1.41 -fun add_del_args add del = syntax
    1.42 -  (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
    1.43 +fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
    1.44 +fun add_del_args add del = syntax (add_del add del);
    1.45  
    1.46  
    1.47