# HG changeset patch
# User wenzelm
# Date 1214680877 -7200
# Node ID cbb4dafea38ad682a509640897e2dd5a24e17b61
# Parent  b1285021424ee985ee43577703fc87289dfaf648
replaced simple_text by fully-featured parse_args;

diff -r b1285021424e -r cbb4dafea38a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Jun 28 21:21:15 2008 +0200
+++ b/src/Pure/Isar/method.ML	Sat Jun 28 21:21:17 2008 +0200
@@ -82,7 +82,6 @@
   val method_setup: bstring -> string * Position.T -> string -> theory -> theory
   val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     -> src -> Proof.context -> 'a * Proof.context
-  val simple_text: Args.T list -> text * Args.T list
   val simple_args: (Args.T list -> 'a * Args.T list)
     -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
@@ -114,6 +113,7 @@
   val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   val parse: OuterLex.token list -> text * OuterLex.token list
+  val parse_args: Args.T list -> text * Args.T list
 end;
 
 structure Method: METHOD =
@@ -474,11 +474,6 @@
 
 fun syntax scan = Args.context_syntax "method" scan;
 
-val simple_text = (Args.$$$ "(" |-- Args.name
-    -- Scan.repeat (Scan.one (fn x => not (Args.string_of x = ")"))) --| Args.$$$ ")"
-  || Args.name -- Scan.succeed [])
-  >> (fn (name, args) => Source (Args.src ((name, args), Position.none)));
-
 fun simple_args scan f src ctxt : method =
   fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
 
@@ -603,14 +598,14 @@
 
 (* outer parser *)
 
-local
-
 structure T = OuterLex;
 structure P = OuterParse;
 
 fun is_symid_meth s =
   s <> "|" andalso s <> "?" andalso s <> "+" andalso T.is_sid s;
 
+local
+
 fun meth4 x =
  (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
   P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
@@ -620,7 +615,7 @@
   meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
   meth4) x
 and meth2 x =
- (P.position (P.xname -- P.args1 is_symid_meth false) >> (Source o Args.src) ||
+ (P.position (P.xname -- P.generic_args1 is_symid_meth) >> (Source o Args.src) ||
   meth3) x
 and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
 and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
@@ -628,6 +623,30 @@
 in val parse = meth3 end;
 
 
+(* args parser *)
+
+local
+
+fun enum1 sep scan = scan ::: Scan.repeat (Args.$$$ sep |-- scan);
+
+fun meth4 x =
+ (Args.position (Args.name >> rpair []) >> (Source o Args.src) ||
+  Args.$$$ "(" |-- Args.!!! (meth0 --| Args.$$$ ")")) x
+and meth3 x =
+ (meth4 --| Args.$$$ "?" >> Try ||
+  meth4 --| Args.$$$ "+" >> Repeat1 ||
+  meth4 -- (Args.$$$ "[" |-- Scan.optional Args.nat 1 --| Args.$$$ "]") >> (SelectGoals o swap) ||
+  meth4) x
+and meth2 x =
+ (Args.position (Args.name -- Args.generic_args1 is_symid_meth) >> (Source o Args.src) ||
+  meth3) x
+and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
+and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
+
+in val parse_args = meth3 end;
+
+
+
 (*final declarations of this structure!*)
 val unfold = unfold_meth;
 val fold = fold_meth;