src/Pure/Isar/args.ML
author wenzelm
Fri, 05 May 2000 21:58:44 +0200
changeset 8803 189203bb4b34
parent 8687 24bff69370f0
child 8896 c80aba8c1d5e
permissions -rw-r--r--
GPLed; added colon, parens;
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
8803
wenzelm
parents: 8687
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     5
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
     6
Concrete argument syntax (of attributes and methods).
5822
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
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     9
signature ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    10
sig
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    11
  type T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    12
  val val_of: T -> string
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    13
  val pos_of: T -> Position.T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    14
  val str_of: T -> string
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    15
  val ident: string * Position.T -> T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    16
  val string: string * Position.T -> T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    17
  val keyword: string * Position.T -> T
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    18
  val stopper: T * (T -> bool)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    19
  val not_eof: T -> bool
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    20
  val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    21
  val !!! : (T list -> 'a) -> T list -> 'a
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    22
  val $$$ : string -> T list -> string * T list
8803
wenzelm
parents: 8687
diff changeset
    23
  val colon: T list -> string * T list
wenzelm
parents: 8687
diff changeset
    24
  val parens: (T list -> 'a * T list) -> T list -> 'a * T list
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    25
  val name: T list -> string * T list
8687
24bff69370f0 Args.name_dummy;
wenzelm
parents: 8549
diff changeset
    26
  val name_dummy: T list -> string option * T list
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    27
  val nat: T list -> int * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    28
  val var: T list -> indexname * T list
6447
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
    29
  val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
    30
  val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
    31
  val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
    32
  val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    33
  val global_typ: theory * T list -> typ * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    34
  val global_term: theory * T list -> term * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    35
  val global_prop: theory * T list -> term * (theory * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    36
  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    37
  val local_term: Proof.context * T list -> term * (Proof.context * T list)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    38
  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
7553
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
    39
  val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
8536
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
    40
  val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
    41
    -> ((int -> tactic) -> tactic) * ('a * T list)
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    42
  type src
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    43
  val src: (string * T list) * Position.T -> src
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    44
  val dest_src: src -> (string * T list) * Position.T
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    45
  val attribs: T list -> src list * T list
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    46
  val opt_attribs: T list -> src list * T list
8282
58a33fd5b30c tuned syntax wrapper;
wenzelm
parents: 8233
diff changeset
    47
  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    48
end;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    49
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    50
structure Args: ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    51
struct
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    52
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    53
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    54
(** datatype T **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    55
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    56
datatype kind = Ident | String | Keyword | EOF;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    57
datatype T = Arg of kind * (string * Position.T);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    58
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    59
fun val_of (Arg (_, (x, _))) = x;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    60
fun pos_of (Arg (_, (_, pos))) = pos;
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 str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    63
  | str_of (Arg (String, (x, _))) = quote x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    64
  | str_of (Arg (Keyword, (x, _))) = x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    65
  | str_of (Arg (EOF, _)) = "end-of-text";
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    66
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    67
fun arg kind x_pos = Arg (kind, x_pos);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    68
val ident = arg Ident;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    69
val string = arg String;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    70
val keyword = arg Keyword;
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
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    73
(* eof *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    74
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    75
val eof = arg EOF ("", Position.none);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    76
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    77
fun is_eof (Arg (EOF, _)) = true
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    78
  | is_eof _ = false;
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
val stopper = (eof, is_eof);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    81
val not_eof = not o is_eof;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    82
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    83
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    84
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    85
(** scanners **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    86
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    87
(* position *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    88
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    89
fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    90
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    91
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    92
(* cut *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    93
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    94
fun !!! scan =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    95
  let
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    96
    fun get_pos [] = " (past end-of-text!)"
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    97
      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    98
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
    99
    fun err (args, None) = "Argument syntax error" ^ get_pos args
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   100
      | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   101
  in Scan.!! err scan end;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   102
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   103
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   104
(* basic *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   105
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   106
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
   107
fun $$$ x = $$$$ x >> val_of;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   108
8803
wenzelm
parents: 8687
diff changeset
   109
val colon = $$$ ":";
wenzelm
parents: 8687
diff changeset
   110
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
wenzelm
parents: 8687
diff changeset
   111
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   112
val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
8687
24bff69370f0 Args.name_dummy;
wenzelm
parents: 8549
diff changeset
   113
val name_dummy = $$$ "_" >> K None || name >> Some;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   114
8233
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   115
val keyword_symid =
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   116
  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   117
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   118
fun kind f = Scan.one (K true) :--
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   119
  (fn Arg (Ident, (x, _)) =>
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   120
    (case f x of Some y => Scan.succeed y | _ => Scan.fail)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   121
  | _ => Scan.fail) >> #2;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   122
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   123
val nat = kind Syntax.read_nat;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   124
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
   125
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   126
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   127
(* enumerations *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   128
6447
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   129
fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   130
fun enum sep scan = enum1 sep scan || Scan.succeed [];
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   131
6447
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   132
fun and_list1 scan = enum1 "and" scan;
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   133
fun and_list scan = enum "and" scan;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   134
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   135
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   136
(* terms and types *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   137
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   138
fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   139
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   140
val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   141
val global_term = gen_item (ProofContext.read_term o ProofContext.init);
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   142
val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   143
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   144
val local_typ = gen_item ProofContext.read_typ;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   145
val local_term = gen_item ProofContext.read_term;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   146
val local_prop = gen_item ProofContext.read_prop;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   147
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   148
7553
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   149
(* bang facts *)
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   150
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   151
val bang_facts = Scan.depend (fn ctxt =>
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   152
  ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   153
af3a1fe87c42 added bang_facts;
wenzelm
parents: 6447
diff changeset
   154
8536
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   155
(* goal specification *)
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   156
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   157
(* range *)
8233
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   158
8536
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   159
val from_to =
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   160
  nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   161
  nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
8549
851d39c10d9f goal_spec: [!];
wenzelm
parents: 8536
diff changeset
   162
  nat >> (fn i => fn tac => tac i) ||
851d39c10d9f goal_spec: [!];
wenzelm
parents: 8536
diff changeset
   163
  $$$$ "!" >> K ALLGOALS;
8536
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   164
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   165
val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
de307f5bc89a goal_spec;
wenzelm
parents: 8282
diff changeset
   166
fun goal_spec def = Scan.lift (Scan.optional goal def);
8233
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   167
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   168
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   169
(* args *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   170
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   171
val exclude = explode "(){}[],";
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   172
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   173
fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   174
  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   175
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   176
fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   177
  >> (fn (x, (ys, z)) => x :: ys @ [z]);
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   178
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   179
fun args blk x = Scan.optional (args1 blk) [] x
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   180
and args1 blk x =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   181
  ((Scan.repeat1
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   182
    (Scan.repeat1 (atom_arg blk) ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   183
      paren_args "(" ")" args ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   184
      paren_args "{" "}" args ||
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   185
      paren_args "[" "]" args)) >> flat) x;
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   186
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   187
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   188
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   189
(** type src **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   190
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   191
datatype src = Src of (string * T list) * Position.T;
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   192
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   193
val src = Src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   194
fun dest_src (Src src) = src;
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   195
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   196
fun err_in_src kind msg (Src ((s, args), pos)) =
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   197
  error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   198
    space_implode " " (map str_of args));
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   199
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   200
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   201
(* argument syntax *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   202
8282
58a33fd5b30c tuned syntax wrapper;
wenzelm
parents: 8233
diff changeset
   203
fun syntax kind scan (src as Src ((s, args), pos)) st =
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   204
  (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   205
    OK (Some x, (st', [])) => (st', x)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   206
  | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
5911
7da8033264fa removed trace;
wenzelm
parents: 5878
diff changeset
   207
  | Error msg => err_in_src kind ("\n" ^ msg) src);
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   208
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   209
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   210
(* attribs *)
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   211
6447
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   212
fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   213
fun list scan = list1 scan || Scan.succeed [];
83d8dabdae9a lifted enum;
wenzelm
parents: 5934
diff changeset
   214
8233
85169951d515 attrib: keyword_symid;
wenzelm
parents: 8089
diff changeset
   215
val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
5878
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   216
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
769abc29bb8e several args parsers;
wenzelm
parents: 5822
diff changeset
   217
val opt_attribs = Scan.optional attribs [];
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   218
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   219
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   220
end;