--- a/src/Pure/General/scan.ML Mon May 10 19:25:42 2004 +0200
+++ b/src/Pure/General/scan.ML Mon May 10 19:25:59 2004 +0200
@@ -30,6 +30,8 @@
val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
(*one element literal*)
val $$ : ''a -> ''a list -> ''a * ''a list
+ (*literal list*)
+ val list: ''a list -> ''a list -> ''a list * ''a list
end;
signature SCAN =
@@ -149,6 +151,14 @@
| $$ a (x :: xs) =
if a = x then (x, xs) else raise FAIL None;
+fun list ys xs =
+ let
+ fun drop_prefix [] xs = xs
+ | drop_prefix (_ :: _) [] = raise MORE None
+ | drop_prefix (y :: ys) (x :: xs) =
+ if y = x then drop_prefix ys xs else raise FAIL None;
+ in (ys, drop_prefix ys xs) end;
+
fun any _ [] = raise MORE None
| any pred (lst as x :: xs) =
if pred x then apfst (cons x) (any pred xs)