# HG changeset patch
# User wenzelm
# Date 957556724 -7200
# Node ID 189203bb4b34974e47211709b637dac6a74bb72f
# Parent  2c37263eb903c574a6fb6f649563f23b3061ec53
GPLed;
added colon, parens;

diff -r 2c37263eb903 -r 189203bb4b34 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri May 05 21:58:18 2000 +0200
+++ b/src/Pure/Isar/args.ML	Fri May 05 21:58:44 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/args.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Concrete argument syntax (of attributes and methods).
 *)
@@ -19,6 +20,8 @@
   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 colon: T list -> string * T list
+  val parens: (T list -> 'a * T list) -> T list -> 'a * T list
   val name: T list -> string * T list
   val name_dummy: T list -> string option * T list
   val nat: T list -> int * T list
@@ -103,6 +106,9 @@
 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
 fun $$$ x = $$$$ x >> val_of;
 
+val colon = $$$ ":";
+fun parens scan = $$$ "(" |-- scan --| $$$ ")";
+
 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
 val name_dummy = $$$ "_" >> K None || name >> Some;