# HG changeset patch
# User wenzelm
# Date 967924353 -7200
# Node ID 58e9d55a9f8834a4270a42bd55baecf1c868bcf3
# Parent  4e47e40c0ac5ed1d99aee0601280d6149ebfdf1f
added mode parser;

diff -r 4e47e40c0ac5 -r 58e9d55a9f88 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Sep 02 21:52:15 2000 +0200
+++ b/src/Pure/Isar/args.ML	Sat Sep 02 21:52:33 2000 +0200
@@ -23,6 +23,7 @@
   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 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
   val nat: T list -> int * T list
@@ -117,6 +118,7 @@
 
 val colon = $$$ ":";
 fun parens 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;
 val name_dummy = $$$ "_" >> K None || name >> Some;