src/Pure/library.ML
changeset 6282 589671bebbb3
parent 5966 60f80b2a2777
child 6312 d361b0a99e31
     1.1 --- a/src/Pure/library.ML	Fri Feb 12 14:40:56 1999 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Feb 13 22:08:54 1999 +0100
     1.3 @@ -122,6 +122,7 @@
     1.4    val string_of_indexname: string * int -> string
     1.5  
     1.6    (*strings*)
     1.7 +  val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
     1.8    val enclose: string -> string -> string -> string
     1.9    val quote: string -> string
    1.10    val space_implode: string -> string list -> string
    1.11 @@ -652,6 +653,13 @@
    1.12  
    1.13  (** strings **)
    1.14  
    1.15 +(*tuned version of foldl for strings, avoids explode*)
    1.16 +fun foldl_string f (x0, str) =
    1.17 +  let
    1.18 +    val n = size str;
    1.19 +    fun fold (x, i) = if i < n then fold (f (x, String.substring (str, i, 1)), i + 1) else x
    1.20 +  in fold (x0, 0) end;
    1.21 +
    1.22  (*enclose in brackets*)
    1.23  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    1.24