1.1 --- a/src/Pure/Isar/args.ML	Sat Jun 28 21:21:13 2008 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Sat Jun 28 21:21:15 2008 +0200
     1.3 @@ -89,6 +89,7 @@
     1.4    val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
     1.5    val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
     1.6      -> ((int -> tactic) -> tactic) * ('a * T list)
     1.7 +  val generic_args1: (string -> bool) -> T list -> T list * T list
     1.8    val attribs: (string -> string) -> T list -> src list * T list
     1.9    val opt_attribs: (string -> string) -> T list -> src list * T list
    1.10    val thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
    1.11 @@ -366,8 +367,6 @@
    1.12  
    1.13  (* goal specification *)
    1.14  
    1.15 -(* range *)
    1.16 -
    1.17  val from_to =
    1.18    nat -- ($$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
    1.19    nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
    1.20 @@ -378,31 +377,34 @@
    1.21  fun goal_spec def = Scan.lift (Scan.optional goal def);
    1.22  
    1.23  
    1.24 -
    1.25 -(* attribs *)
    1.26 +(* nested args and attribs *)
    1.27  
    1.28  local
    1.29  
    1.30 -val exclude = member (op =) (explode "()[],");
    1.31 +fun parse_args is_symid =
    1.32 +  let
    1.33 +    fun atom blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
    1.34 +      k <> Keyword orelse is_symid x orelse blk andalso x = ","));
    1.35  
    1.36 -fun atomic blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
    1.37 -    k <> Keyword orelse not (exclude x) orelse blk andalso x = ","));
    1.38 -
    1.39 -fun args blk x = Scan.optional (args1 blk) [] x
    1.40 -and args1 blk x =
    1.41 -  ((Scan.repeat1
    1.42 -    (Scan.repeat1 (atomic blk) ||
    1.43 -      argsp "(" ")" ||
    1.44 -      argsp "[" "]")) >> flat) x
    1.45 -and argsp l r x =
    1.46 -  (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
    1.47 +    fun args blk x = Scan.optional (args1 blk) [] x
    1.48 +    and args1 blk x =
    1.49 +      ((Scan.repeat1
    1.50 +        (Scan.repeat1 (atom blk) ||
    1.51 +          argsp "(" ")" ||
    1.52 +          argsp "[" "]")) >> flat) x
    1.53 +    and argsp l r x =
    1.54 +      (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
    1.55 +  in (args, args1) end;
    1.56  
    1.57  in
    1.58  
    1.59 +fun generic_args1 is_symid = #2 (parse_args is_symid) false;
    1.60 +val arguments = #1 (parse_args OuterLex.is_sid) false;
    1.61 +
    1.62  fun attribs intern =
    1.63    let
    1.64      val attrib_name = internal_text || (symbolic || named) >> evaluate Text intern;
    1.65 -    val attrib = position (attrib_name -- !!! (args false)) >> src;
    1.66 +    val attrib = position (attrib_name -- !!! arguments) >> src;
    1.67    in $$$ "[" |-- !!! (list attrib --| $$$ "]") end;
    1.68  
    1.69  fun opt_attribs intern = Scan.optional (attribs intern) [];
    1.70 @@ -417,7 +419,9 @@
    1.71    Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []);
    1.72  
    1.73  
    1.74 -(* syntax interface *)
    1.75 +
    1.76 +
    1.77 +(** syntax wrapper **)
    1.78  
    1.79  fun syntax kind scan (src as Src ((s, args), pos)) st =
    1.80    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of