# HG changeset patch
# User wenzelm
# Date 970685757 -7200
# Node ID a068c666c53ef06c39b20ef48bf189913b57ca9d
# Parent  7cfdf6a330a04a00e685b7835107a3f8adedc294
added "bracks";

diff -r 7cfdf6a330a0 -r a068c666c53e src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Oct 04 17:35:45 2000 +0200
+++ b/src/Pure/Isar/args.ML	Wed Oct 04 20:55:57 2000 +0200
@@ -29,6 +29,7 @@
   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 bracks: (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
   val name_dummy: T list -> string option * T list
@@ -131,6 +132,7 @@
 val bang_colon = $$$ "!:";
 
 fun parens scan = $$$ "(" |-- scan --| $$$ ")";
+fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
 fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
 
 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;