--- a/src/Pure/library.ML Tue Mar 09 12:06:09 1999 +0100
+++ b/src/Pure/library.ML Tue Mar 09 12:07:16 1999 +0100
@@ -122,7 +122,9 @@
val string_of_indexname: string * int -> string
(*strings*)
+ val nth_elem_string: int * string -> string
val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
+ val exists_string: (string -> bool) -> string -> bool
val enclose: string -> string -> string -> string
val quote: string -> string
val space_implode: string -> string list -> string
@@ -653,13 +655,19 @@
(** strings **)
-(*tuned version of foldl for strings, avoids explode*)
+(*functions tuned for strings, avoiding explode*)
+
+fun nth_elem_string (i, str) =
+ String.substring (str, i, 1) handle _ => raise LIST "nth_elem_string";
+
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;
+fun exists_string pred str = foldl_string (fn (b, s) => b orelse pred s) (false, str);
+
(*enclose in brackets*)
fun enclose lpar rpar str = lpar ^ str ^ rpar;