# HG changeset patch
# User wenzelm
# Date 911046260 -3600
# Node ID 7536314d9a5fc251c21c3a977695b20371368f9c
# Parent  ed11c98908527e5a32cfe5bf16372efbd7e7e048
added unless, first;

diff -r ed11c9890852 -r 7536314d9a5f src/Pure/Syntax/scan.ML
--- a/src/Pure/Syntax/scan.ML	Sat Nov 14 13:23:49 1998 +0100
+++ b/src/Pure/Syntax/scan.ML	Sat Nov 14 13:24:20 1998 +0100
@@ -37,6 +37,8 @@
   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
+  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
+  val first: ('a -> 'b) list -> 'a -> 'b
   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
@@ -132,6 +134,12 @@
 
 fun ahead scan xs = (fst (scan xs), xs);
 
+fun unless test scan =
+  ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
+
+fun first [] = fail
+  | first (scan :: scans) = scan || first scans;
+
 
 (* state based scanners *)