src/Pure/Isar/args.ML
author wenzelm
Mon, 16 Nov 1998 11:02:07 +0100
changeset 5878 769abc29bb8e
parent 5822 3f824514ad88
child 5911 7da8033264fa
permissions -rw-r--r--
several args parsers; include positions; misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/args.ML
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     4
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
     5
Concrete argument syntax (of attributes and methods).
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     6
*)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     7
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     8
signature ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     9
sig
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    10
  type T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    11
  val val_of: T -> string
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    12
  val pos_of: T -> Position.T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    13
  val str_of: T -> string
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    14
  val ident: string * Position.T -> T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    15
  val string: string * Position.T -> T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    16
  val keyword: string * Position.T -> T
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    17
  val stopper: T * (T -> bool)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    18
  val not_eof: T -> bool
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    19
  val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    20
  val !!! : (T list -> 'a) -> T list -> 'a
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    21
  val $$$ : string -> T list -> string * T list
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    22
  val name: T list -> string * T list
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    23
  val nat: T list -> int * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    24
  val var: T list -> indexname * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    25
  val enum1: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    26
  val enum: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    27
  val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    28
  val list: (T list -> 'a * T list) -> T list -> 'a list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    29
  val global_typ: theory * T list -> typ * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    30
  val global_term: theory * T list -> term * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    31
  val global_prop: theory * T list -> term * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    32
  val global_pat: theory * T list -> term * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    33
  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    34
  val local_term: Proof.context * T list -> term * (Proof.context * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    35
  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    36
  val local_pat: Proof.context * T list -> term * (Proof.context * T list)
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    37
  type src
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    38
  val src: (string * T list) * Position.T -> src
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    39
  val dest_src: src -> (string * T list) * Position.T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    40
  val attribs: T list -> src list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    41
  val opt_attribs: T list -> src list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    42
  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    43
end;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    44
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    45
structure Args: ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    46
struct
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    47
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    48
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    49
(** datatype T **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    50
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    51
datatype kind = Ident | String | Keyword | EOF;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    52
datatype T = Arg of kind * (string * Position.T);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    53
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    54
fun val_of (Arg (_, (x, _))) = x;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    55
fun pos_of (Arg (_, (_, pos))) = pos;
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    56
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    57
fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    58
  | str_of (Arg (String, (x, _))) = quote x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    59
  | str_of (Arg (Keyword, (x, _))) = x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    60
  | str_of (Arg (EOF, _)) = "end-of-text";
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    61
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    62
fun arg kind x_pos = Arg (kind, x_pos);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    63
val ident = arg Ident;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    64
val string = arg String;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    65
val keyword = arg Keyword;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    66
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    67
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    68
(* eof *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    69
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    70
val eof = arg EOF ("", Position.none);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    71
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    72
fun is_eof (Arg (EOF, _)) = true
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    73
  | is_eof _ = false;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    74
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    75
val stopper = (eof, is_eof);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    76
val not_eof = not o is_eof;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    77
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    78
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    79
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    80
(** scanners **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    81
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    82
(* position *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    83
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    84
fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    85
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    86
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    87
(* cut *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    88
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    89
fun !!! scan =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    90
  let
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    91
    fun get_pos [] = " (past end-of-text!)"
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    92
      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    93
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    94
    fun err (args, None) = "Argument syntax error" ^ get_pos args
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    95
      | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    96
  in Scan.!! err scan end;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    97
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    98
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    99
(* basic *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   100
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   101
fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   102
fun $$$ x = $$$$ x >> val_of;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   103
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   104
val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   105
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   106
fun kind f = Scan.one (K true) :--
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   107
  (fn Arg (Ident, (x, _)) =>
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   108
    (case f x of Some y => Scan.succeed y | _ => Scan.fail)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   109
  | _ => Scan.fail) >> #2;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   110
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   111
val nat = kind Syntax.read_nat;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   112
val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   113
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   114
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   115
(* enumerations *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   116
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   117
fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   118
fun enum sep scan = enum1 sep scan || Scan.succeed [];
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   119
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   120
fun list1 scan = enum1 "," scan;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   121
fun list scan = enum "," scan;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   122
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   123
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   124
(* terms and types *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   125
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   126
fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   127
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   128
val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   129
val global_term = gen_item (ProofContext.read_term o ProofContext.init);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   130
val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   131
val global_pat = gen_item (ProofContext.read_pat o ProofContext.init);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   132
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   133
val local_typ = gen_item ProofContext.read_typ;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   134
val local_term = gen_item ProofContext.read_term;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   135
val local_prop = gen_item ProofContext.read_prop;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   136
val local_pat = gen_item ProofContext.read_pat;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   137
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   138
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   139
(* args *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   140
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   141
val exclude = explode "(){}[],";
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   142
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   143
fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   144
  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   145
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   146
fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   147
  >> (fn (x, (ys, z)) => x :: ys @ [z]);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   148
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   149
fun args blk x = Scan.optional (args1 blk) [] x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   150
and args1 blk x =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   151
  ((Scan.repeat1
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   152
    (Scan.repeat1 (atom_arg blk) ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   153
      paren_args "(" ")" args ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   154
      paren_args "{" "}" args ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   155
      paren_args "[" "]" args)) >> flat) x;
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   156
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   157
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   158
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   159
(** type src **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   160
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   161
datatype src = Src of (string * T list) * Position.T;
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   162
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   163
val src = Src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   164
fun dest_src (Src src) = src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   165
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   166
fun err_in_src kind msg (Src ((s, args), pos)) =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   167
  error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   168
    space_implode " " (map str_of args));
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   169
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   170
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   171
(* argument syntax *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   172
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   173
(* FIXME *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   174
fun trace_src kind (Src ((s, args), pos)) =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   175
  warning ("TRACE: " ^ space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   176
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   177
fun syntax kind scan st (src as Src ((s, args), pos)) =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   178
  (trace_src kind src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   179
  (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   180
    OK (Some x, (st', [])) => (st', x)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   181
  | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   182
  | Error msg => err_in_src kind ("\n" ^ msg) src));
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   183
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   184
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   185
(* attribs *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   186
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   187
val attrib = position (name -- !!! (args false)) >> src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   188
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   189
val opt_attribs = Scan.optional attribs [];
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   190
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   191
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   192
end;