# HG changeset patch
# User wenzelm
# Date 969400465 -7200
# Node ID c095955e7575879c16f9016e3635c34e79de21b1
# Parent  4bca6b2d258939034934790048f51a74281cdbcb
added common args keywords;

diff -r 4bca6b2d2589 -r c095955e7575 src/Pure/Isar/args.ML
--- 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 *)