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