added common args keywords;
authorwenzelm
Tue Sep 19 23:54:25 2000 +0200 (2000-09-19)
changeset 10035c095955e7575
parent 10034 4bca6b2d2589
child 10036 ca83cc2973f9
added common args keywords;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Tue Sep 19 23:53:00 2000 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Sep 19 23:54:25 2000 +0200
     1.3 @@ -21,7 +21,13 @@
     1.4    val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
     1.5    val !!! : (T list -> 'a) -> T list -> 'a
     1.6    val $$$ : string -> T list -> string * T list
     1.7 +  val add: T list -> string * T list
     1.8 +  val del: T list -> string * T list
     1.9    val colon: T list -> string * T list
    1.10 +  val query: T list -> string * T list
    1.11 +  val bang: T list -> string * T list
    1.12 +  val query_colon: T list -> string * T list
    1.13 +  val bang_colon: T list -> string * T list
    1.14    val parens: (T list -> 'a * T list) -> T list -> 'a * T list
    1.15    val mode: string -> 'a * T list -> bool * ('a * T list)
    1.16    val name: T list -> string * T list
    1.17 @@ -29,8 +35,6 @@
    1.18    val nat: T list -> int * T list
    1.19    val int: T list -> int * T list
    1.20    val var: T list -> indexname * T list
    1.21 -  val addN: string
    1.22 -  val delN: string
    1.23    val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    1.24    val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    1.25    val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    1.26 @@ -118,7 +122,14 @@
    1.27  fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
    1.28  fun $$$ x = $$$$ x >> val_of;
    1.29  
    1.30 +val add = $$$ "add";
    1.31 +val del = $$$ "del";
    1.32  val colon = $$$ ":";
    1.33 +val query = $$$ "?";
    1.34 +val bang = $$$ "!";
    1.35 +val query_colon = $$$ "?:";
    1.36 +val bang_colon = $$$ "!:";
    1.37 +
    1.38  fun parens scan = $$$ "(" |-- scan --| $$$ ")";
    1.39  fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
    1.40  
    1.41 @@ -137,9 +148,6 @@
    1.42  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
    1.43  val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
    1.44  
    1.45 -val addN = "add";
    1.46 -val delN = "del";
    1.47 -
    1.48  
    1.49  (* enumerations *)
    1.50