--- 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 *)