src/Pure/Isar/method.ML
changeset 7268 315655dc361b
parent 7130 a17f7b5ac40f
child 7367 a79d4683fadf
     1.1 --- a/src/Pure/Isar/method.ML	Wed Aug 18 20:42:09 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 18 20:43:42 1999 +0200
     1.3 @@ -36,14 +36,15 @@
     1.4    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     1.5      Proof.context -> Args.src -> Proof.context * 'a
     1.6    val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
     1.7 -  val sectioned_args: ((Args.T list -> Proof.context attribute * Args.T list) list ->
     1.8 +  type modifier
     1.9 +  val sectioned_args: ((Args.T list -> modifier * Args.T list) list ->
    1.10        Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.11 -    (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.12 +    (Args.T list -> modifier * Args.T list) list ->
    1.13      ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.14 -  val default_sectioned_args: Proof.context attribute ->
    1.15 -    (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.16 +  val default_sectioned_args: modifier ->
    1.17 +    (Args.T list -> modifier * Args.T list) list ->
    1.18      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.19 -  val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.20 +  val only_sectioned_args: (Args.T list -> modifier * Args.T list) list ->
    1.21      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.22    val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.23    datatype text =
    1.24 @@ -241,28 +242,36 @@
    1.25  
    1.26  (* sections *)
    1.27  
    1.28 +type modifier = (Proof.context -> Proof.context) * Proof.context attribute;
    1.29 +
    1.30 +local
    1.31 +
    1.32  fun sect ss = Scan.first (map (fn s => Scan.lift (s --| Args.$$$ ":")) ss);
    1.33  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    1.34  fun thmss ss = Scan.repeat (thms ss) >> flat;
    1.35  
    1.36 -fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]);
    1.37 +fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]);
    1.38  
    1.39 -fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt =>
    1.40 -  Scan.succeed (apply att (ctxt, ths)))) >> #2;
    1.41 +fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    1.42 +  Scan.succeed (apply m (ctxt, ths)))) >> #2;
    1.43  
    1.44  fun sectioned args ss = args ss -- Scan.repeat (section ss);
    1.45  
    1.46 +in
    1.47  
    1.48  fun sectioned_args args ss f src ctxt =
    1.49    let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
    1.50    in f x ctxt' end;
    1.51  
    1.52 -fun default_sectioned_args att ss f src ctxt =
    1.53 -  sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply att (ctxt', ths)))) src ctxt;
    1.54 +fun default_sectioned_args m ss f src ctxt =
    1.55 +  sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply m (ctxt', ths)))) src ctxt;
    1.56  
    1.57  fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f);
    1.58 +
    1.59  fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths);
    1.60  
    1.61 +end;
    1.62 +
    1.63  
    1.64  
    1.65  (** method text **)