# HG changeset patch
# User wenzelm
# Date 918940134 -3600
# Node ID 589671bebbb37ef5aaa1928dcbf0f6cb438a2386
# Parent  25d41c1183041550446e352279423b8a58021081
foldl_string;

diff -r 25d41c118304 -r 589671bebbb3 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Feb 12 14:40:56 1999 +0100
+++ b/src/Pure/library.ML	Sat Feb 13 22:08:54 1999 +0100
@@ -122,6 +122,7 @@
   val string_of_indexname: string * int -> string
 
   (*strings*)
+  val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
   val enclose: string -> string -> string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
@@ -652,6 +653,13 @@
 
 (** strings **)
 
+(*tuned version of foldl for strings, avoids explode*)
+fun foldl_string f (x0, str) =
+  let
+    val n = size str;
+    fun fold (x, i) = if i < n then fold (f (x, String.substring (str, i, 1)), i + 1) else x
+  in fold (x0, 0) end;
+
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;