1.1 --- a/src/Pure/Isar/args.ML	Mon Nov 16 11:00:58 1998 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Nov 16 11:02:07 1998 +0100
     1.3 @@ -2,26 +2,44 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Concrete argument syntax (for attributes, methods etc.).
     1.8 -
     1.9 -TODO:
    1.10 -  - sectioned: generalize sname to attributed thms;
    1.11 +Concrete argument syntax (of attributes and methods).
    1.12  *)
    1.13  
    1.14  signature ARGS =
    1.15  sig
    1.16    type T
    1.17    val val_of: T -> string
    1.18 -  val ident: string -> T
    1.19 -  val string: string -> T
    1.20 -  val keyword: string -> T
    1.21 +  val pos_of: T -> Position.T
    1.22 +  val str_of: T -> string
    1.23 +  val ident: string * Position.T -> T
    1.24 +  val string: string * Position.T -> T
    1.25 +  val keyword: string * Position.T -> T
    1.26    val stopper: T * (T -> bool)
    1.27    val not_eof: T -> bool
    1.28 +  val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    1.29 +  val !!! : (T list -> 'a) -> T list -> 'a
    1.30    val $$$ : string -> T list -> string * T list
    1.31    val name: T list -> string * T list
    1.32 -  val sectioned: string list -> T list -> (string list * (string * string list) list) * T list
    1.33 +  val nat: T list -> int * T list
    1.34 +  val var: T list -> indexname * T list
    1.35 +  val enum1: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
    1.36 +  val enum: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
    1.37 +  val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
    1.38 +  val list: (T list -> 'a * T list) -> T list -> 'a list * T list
    1.39 +  val global_typ: theory * T list -> typ * (theory * T list)
    1.40 +  val global_term: theory * T list -> term * (theory * T list)
    1.41 +  val global_prop: theory * T list -> term * (theory * T list)
    1.42 +  val global_pat: theory * T list -> term * (theory * T list)
    1.43 +  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
    1.44 +  val local_term: Proof.context * T list -> term * (Proof.context * T list)
    1.45 +  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    1.46 +  val local_pat: Proof.context * T list -> term * (Proof.context * T list)
    1.47    type src
    1.48 -  val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b
    1.49 +  val src: (string * T list) * Position.T -> src
    1.50 +  val dest_src: src -> (string * T list) * Position.T
    1.51 +  val attribs: T list -> src list * T list
    1.52 +  val opt_attribs: T list -> src list * T list
    1.53 +  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
    1.54  end;
    1.55  
    1.56  structure Args: ARGS =
    1.57 @@ -31,15 +49,17 @@
    1.58  (** datatype T **)
    1.59  
    1.60  datatype kind = Ident | String | Keyword | EOF;
    1.61 -datatype T = Arg of kind * string;
    1.62 +datatype T = Arg of kind * (string * Position.T);
    1.63  
    1.64 -fun val_of (Arg (_, x)) = x;
    1.65 +fun val_of (Arg (_, (x, _))) = x;
    1.66 +fun pos_of (Arg (_, (_, pos))) = pos;
    1.67  
    1.68 -fun str_of (Arg (Ident, x)) = enclose "'" "'" x
    1.69 -  | str_of (Arg (String, x)) = quote x
    1.70 -  | str_of (Arg (Keyword, x)) = x;
    1.71 +fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
    1.72 +  | str_of (Arg (String, (x, _))) = quote x
    1.73 +  | str_of (Arg (Keyword, (x, _))) = x
    1.74 +  | str_of (Arg (EOF, _)) = "end-of-text";
    1.75  
    1.76 -fun arg kind x = Arg (kind, x);
    1.77 +fun arg kind x_pos = Arg (kind, x_pos);
    1.78  val ident = arg Ident;
    1.79  val string = arg String;
    1.80  val keyword = arg Keyword;
    1.81 @@ -47,7 +67,7 @@
    1.82  
    1.83  (* eof *)
    1.84  
    1.85 -val eof = arg EOF "";
    1.86 +val eof = arg EOF ("", Position.none);
    1.87  
    1.88  fun is_eof (Arg (EOF, _)) = true
    1.89    | is_eof _ = false;
    1.90 @@ -59,42 +79,114 @@
    1.91  
    1.92  (** scanners **)
    1.93  
    1.94 +(* position *)
    1.95 +
    1.96 +fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
    1.97 +
    1.98 +
    1.99 +(* cut *)
   1.100 +
   1.101 +fun !!! scan =
   1.102 +  let
   1.103 +    fun get_pos [] = " (past end-of-text!)"
   1.104 +      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
   1.105 +
   1.106 +    fun err (args, None) = "Argument syntax error" ^ get_pos args
   1.107 +      | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
   1.108 +  in Scan.!! err scan end;
   1.109 +
   1.110 +
   1.111  (* basic *)
   1.112  
   1.113 -fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of;
   1.114 -val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of;
   1.115 +fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   1.116 +fun $$$ x = $$$$ x >> val_of;
   1.117 +
   1.118 +val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   1.119 +
   1.120 +fun kind f = Scan.one (K true) :--
   1.121 +  (fn Arg (Ident, (x, _)) =>
   1.122 +    (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   1.123 +  | _ => Scan.fail) >> #2;
   1.124 +
   1.125 +val nat = kind Syntax.read_nat;
   1.126 +val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
   1.127  
   1.128  
   1.129 -(* sections *)
   1.130 +(* enumerations *)
   1.131 +
   1.132 +fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
   1.133 +fun enum sep scan = enum1 sep scan || Scan.succeed [];
   1.134 +
   1.135 +fun list1 scan = enum1 "," scan;
   1.136 +fun list scan = enum "," scan;
   1.137 +
   1.138  
   1.139 -val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":");
   1.140 -val sname = name --| Scan.ahead no_colon;
   1.141 +(* terms and types *)
   1.142 +
   1.143 +fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
   1.144 +
   1.145 +val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
   1.146 +val global_term = gen_item (ProofContext.read_term o ProofContext.init);
   1.147 +val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
   1.148 +val global_pat = gen_item (ProofContext.read_pat o ProofContext.init);
   1.149  
   1.150 -fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname;
   1.151 +val local_typ = gen_item ProofContext.read_typ;
   1.152 +val local_term = gen_item ProofContext.read_term;
   1.153 +val local_prop = gen_item ProofContext.read_prop;
   1.154 +val local_pat = gen_item ProofContext.read_pat;
   1.155 +
   1.156 +
   1.157 +(* args *)
   1.158 +
   1.159 +val exclude = explode "(){}[],";
   1.160  
   1.161 -fun any_sect [] = Scan.fail
   1.162 -  | any_sect (s :: ss) = sect s || any_sect ss;
   1.163 +fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   1.164 +  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
   1.165 +
   1.166 +fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
   1.167 +  >> (fn (x, (ys, z)) => x :: ys @ [z]);
   1.168  
   1.169 -fun sectioned ss =
   1.170 -  Scan.repeat sname -- Scan.repeat (any_sect ss);
   1.171 +fun args blk x = Scan.optional (args1 blk) [] x
   1.172 +and args1 blk x =
   1.173 +  ((Scan.repeat1
   1.174 +    (Scan.repeat1 (atom_arg blk) ||
   1.175 +      paren_args "(" ")" args ||
   1.176 +      paren_args "{" "}" args ||
   1.177 +      paren_args "[" "]" args)) >> flat) x;
   1.178  
   1.179  
   1.180  
   1.181  (** type src **)
   1.182  
   1.183 -type src = (string * T list) * Position.T;
   1.184 +datatype src = Src of (string * T list) * Position.T;
   1.185  
   1.186 -fun err_in_src kind msg ((s, args), pos) =
   1.187 -  error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg);
   1.188 +val src = Src;
   1.189 +fun dest_src (Src src) = src;
   1.190 +
   1.191 +fun err_in_src kind msg (Src ((s, args), pos)) =
   1.192 +  error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
   1.193 +    space_implode " " (map str_of args));
   1.194  
   1.195  
   1.196  (* argument syntax *)
   1.197  
   1.198 -fun syntax kind scan f (src as ((s, args), pos)) =
   1.199 -  (case handle_error (Scan.error (Scan.finite stopper scan)) args of
   1.200 -    OK (x, []) => f x
   1.201 -  | OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos)
   1.202 -  | Error msg => err_in_src kind ("\n" ^ msg) src);
   1.203 +(* FIXME *)
   1.204 +fun trace_src kind (Src ((s, args), pos)) =
   1.205 +  warning ("TRACE: " ^ space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos);
   1.206 +
   1.207 +fun syntax kind scan st (src as Src ((s, args), pos)) =
   1.208 +  (trace_src kind src;
   1.209 +  (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
   1.210 +    OK (Some x, (st', [])) => (st', x)
   1.211 +  | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
   1.212 +  | Error msg => err_in_src kind ("\n" ^ msg) src));
   1.213 +
   1.214 +
   1.215 +(* attribs *)
   1.216 +
   1.217 +val attrib = position (name -- !!! (args false)) >> src;
   1.218 +val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
   1.219 +val opt_attribs = Scan.optional attribs [];
   1.220  
   1.221  
   1.222  end;