--- a/src/Pure/Isar/args.ML Tue Sep 19 23:53:00 2000 +0200
+++ b/src/Pure/Isar/args.ML Tue Sep 19 23:54:25 2000 +0200
@@ -21,7 +21,13 @@
val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
val !!! : (T list -> 'a) -> T list -> 'a
val $$$ : string -> T list -> string * T list
+ val add: T list -> string * T list
+ val del: T list -> string * T list
val colon: T list -> string * T list
+ val query: T list -> string * T list
+ val bang: T list -> string * T list
+ val query_colon: T list -> string * T list
+ val bang_colon: T list -> string * T list
val parens: (T list -> 'a * T list) -> T list -> 'a * T list
val mode: string -> 'a * T list -> bool * ('a * T list)
val name: T list -> string * T list
@@ -29,8 +35,6 @@
val nat: T list -> int * T list
val int: T list -> int * T list
val var: T list -> indexname * T list
- val addN: string
- val delN: string
val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
@@ -118,7 +122,14 @@
fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
fun $$$ x = $$$$ x >> val_of;
+val add = $$$ "add";
+val del = $$$ "del";
val colon = $$$ ":";
+val query = $$$ "?";
+val bang = $$$ "!";
+val query_colon = $$$ "?:";
+val bang_colon = $$$ "!:";
+
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
@@ -137,9 +148,6 @@
val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
-val addN = "add";
-val delN = "del";
-
(* enumerations *)