# HG changeset patch
# User berghofe
# Date 1043858111 -3600
# Node ID cfa3441c5238abd5d3bdb91f0e2a95c1fc59df52
# Parent  332eb2e69a65dd1e31d2e92a11cb454d05b9f2ad
Some tuning:
- finite now uses rev_append (tail recursive!) to append stopper, because @
  needs to much stack space for large strings
- repeat is now tail recursive

diff -r 332eb2e69a65 -r cfa3441c5238 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed Jan 29 17:32:19 2003 +0100
+++ b/src/Pure/General/scan.ML	Wed Jan 29 17:35:11 2003 +0100
@@ -124,7 +124,11 @@
 fun optional scan def = scan || succeed def;
 fun option scan = optional (scan >> Some) None;
 
-fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
+fun repeat scan =
+  let fun rep ys xs = (case (Some (scan xs) handle FAIL _ => None) of
+    None => (rev ys, xs) | Some (y, xs') => rep (y :: ys) xs')
+  in rep [] end;
+
 fun repeat1 scan = scan -- repeat scan >> op ::;
 
 fun max leq scan1 scan2 xs =
@@ -184,7 +188,7 @@
   in
     if exists is_stopper input then
       raise ABORT "Stopper may not occur in input of finite scan!"
-    else (force scan --| lift stop) (state, input @ [stopper])
+    else (force scan --| lift stop) (state, rev_append (rev input) [stopper])
   end;
 
 fun finite stopper scan xs =