replaced simple_text by fully-featured parse_args;
authorwenzelm
Sat Jun 28 21:21:17 2008 +0200 (2008-06-28)
changeset 27383cbb4dafea38a
parent 27382 b1285021424e
child 27384 bbb68fea688f
replaced simple_text by fully-featured parse_args;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Sat Jun 28 21:21:15 2008 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Jun 28 21:21:17 2008 +0200
     1.3 @@ -82,7 +82,6 @@
     1.4    val method_setup: bstring -> string * Position.T -> string -> theory -> theory
     1.5    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     1.6      -> src -> Proof.context -> 'a * Proof.context
     1.7 -  val simple_text: Args.T list -> text * Args.T list
     1.8    val simple_args: (Args.T list -> 'a * Args.T list)
     1.9      -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
    1.10    val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
    1.11 @@ -114,6 +113,7 @@
    1.12    val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.13      (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
    1.14    val parse: OuterLex.token list -> text * OuterLex.token list
    1.15 +  val parse_args: Args.T list -> text * Args.T list
    1.16  end;
    1.17  
    1.18  structure Method: METHOD =
    1.19 @@ -474,11 +474,6 @@
    1.20  
    1.21  fun syntax scan = Args.context_syntax "method" scan;
    1.22  
    1.23 -val simple_text = (Args.$$$ "(" |-- Args.name
    1.24 -    -- Scan.repeat (Scan.one (fn x => not (Args.string_of x = ")"))) --| Args.$$$ ")"
    1.25 -  || Args.name -- Scan.succeed [])
    1.26 -  >> (fn (name, args) => Source (Args.src ((name, args), Position.none)));
    1.27 -
    1.28  fun simple_args scan f src ctxt : method =
    1.29    fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
    1.30  
    1.31 @@ -603,14 +598,14 @@
    1.32  
    1.33  (* outer parser *)
    1.34  
    1.35 -local
    1.36 -
    1.37  structure T = OuterLex;
    1.38  structure P = OuterParse;
    1.39  
    1.40  fun is_symid_meth s =
    1.41    s <> "|" andalso s <> "?" andalso s <> "+" andalso T.is_sid s;
    1.42  
    1.43 +local
    1.44 +
    1.45  fun meth4 x =
    1.46   (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
    1.47    P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
    1.48 @@ -620,7 +615,7 @@
    1.49    meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
    1.50    meth4) x
    1.51  and meth2 x =
    1.52 - (P.position (P.xname -- P.args1 is_symid_meth false) >> (Source o Args.src) ||
    1.53 + (P.position (P.xname -- P.generic_args1 is_symid_meth) >> (Source o Args.src) ||
    1.54    meth3) x
    1.55  and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.56  and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.57 @@ -628,6 +623,30 @@
    1.58  in val parse = meth3 end;
    1.59  
    1.60  
    1.61 +(* args parser *)
    1.62 +
    1.63 +local
    1.64 +
    1.65 +fun enum1 sep scan = scan ::: Scan.repeat (Args.$$$ sep |-- scan);
    1.66 +
    1.67 +fun meth4 x =
    1.68 + (Args.position (Args.name >> rpair []) >> (Source o Args.src) ||
    1.69 +  Args.$$$ "(" |-- Args.!!! (meth0 --| Args.$$$ ")")) x
    1.70 +and meth3 x =
    1.71 + (meth4 --| Args.$$$ "?" >> Try ||
    1.72 +  meth4 --| Args.$$$ "+" >> Repeat1 ||
    1.73 +  meth4 -- (Args.$$$ "[" |-- Scan.optional Args.nat 1 --| Args.$$$ "]") >> (SelectGoals o swap) ||
    1.74 +  meth4) x
    1.75 +and meth2 x =
    1.76 + (Args.position (Args.name -- Args.generic_args1 is_symid_meth) >> (Source o Args.src) ||
    1.77 +  meth3) x
    1.78 +and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.79 +and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.80 +
    1.81 +in val parse_args = meth3 end;
    1.82 +
    1.83 +
    1.84 +
    1.85  (*final declarations of this structure!*)
    1.86  val unfold = unfold_meth;
    1.87  val fold = fold_meth;