tuned syntax wrapper;
authorwenzelm
Tue Feb 22 21:51:25 2000 +0100 (2000-02-22)
changeset 828258a33fd5b30c
parent 8281 188e2924433e
child 8283 0a319c5746eb
tuned syntax wrapper;
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/args.ML	Tue Feb 22 21:50:02 2000 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Feb 22 21:51:25 2000 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    val dest_src: src -> (string * T list) * Position.T
     1.5    val attribs: T list -> src list * T list
     1.6    val opt_attribs: T list -> src list * T list
     1.7 -  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
     1.8 +  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
     1.9  end;
    1.10  
    1.11  structure Args: ARGS =
    1.12 @@ -183,7 +183,7 @@
    1.13  
    1.14  (* argument syntax *)
    1.15  
    1.16 -fun syntax kind scan st (src as Src ((s, args), pos)) =
    1.17 +fun syntax kind scan (src as Src ((s, args), pos)) st =
    1.18    (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
    1.19      OK (Some x, (st', [])) => (st', x)
    1.20    | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
     2.1 --- a/src/Pure/Isar/attrib.ML	Tue Feb 22 21:50:02 2000 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Tue Feb 22 21:51:25 2000 +0100
     2.3 @@ -157,7 +157,7 @@
     2.4  (** attribute syntax **)
     2.5  
     2.6  fun syntax scan src (st, th) =
     2.7 -  let val (st', f) = Args.syntax "attribute" scan st src
     2.8 +  let val (st', f) = Args.syntax "attribute" scan src st
     2.9    in f (st', th) end;
    2.10  
    2.11  fun no_args x = syntax (Scan.succeed x);
     3.1 --- a/src/Pure/Isar/method.ML	Tue Feb 22 21:50:02 2000 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Tue Feb 22 21:51:25 2000 +0100
     3.3 @@ -50,7 +50,7 @@
     3.4    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     3.5      -> theory -> theory
     3.6    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     3.7 -    Proof.context -> Args.src -> Proof.context * 'a
     3.8 +    Args.src -> Proof.context -> Proof.context * 'a
     3.9    val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    3.10    val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
    3.11    type modifier
    3.12 @@ -403,7 +403,7 @@
    3.13    Args.syntax "method" scan;
    3.14  
    3.15  fun ctxt_args (f: Proof.context -> Proof.method) src ctxt =
    3.16 -  #2 (syntax (Scan.succeed (f ctxt)) ctxt src);
    3.17 +  #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
    3.18  
    3.19  fun no_args m = ctxt_args (K m);
    3.20  
    3.21 @@ -428,7 +428,7 @@
    3.22  in
    3.23  
    3.24  fun sectioned_args args ss f src ctxt =
    3.25 -  let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
    3.26 +  let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt
    3.27    in f x ctxt' end;
    3.28  
    3.29  fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
    3.30 @@ -447,7 +447,7 @@
    3.31      Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --
    3.32      (Scan.lift (Args.$$$ "in") |-- Attrib.local_thm);
    3.33  
    3.34 -fun inst_args f src ctxt = f ((#2 oo syntax insts) ctxt src);
    3.35 +fun inst_args f = f oo (#2 oo syntax insts);
    3.36  
    3.37  
    3.38