# HG changeset patch
# User wenzelm
# Date 1084209959 -7200
# Node ID 9657c23cc3e7d73bcf067a3fabf2cb430373542d
# Parent  2ed5b960c6b10bb30adc63a6137ed7cf6e473262
added Scan.list;

diff -r 2ed5b960c6b1 -r 9657c23cc3e7 src/Pure/General/scan.ML
--- 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)