added nth_elem_string, exists_string;
authorwenzelm
Tue Mar 09 12:07:16 1999 +0100 (1999-03-09)
changeset 6312d361b0a99e31
parent 6311 15652e058e28
child 6313 6e4c7209ff39
added nth_elem_string, exists_string;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Mar 09 12:06:09 1999 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Mar 09 12:07:16 1999 +0100
     1.3 @@ -122,7 +122,9 @@
     1.4    val string_of_indexname: string * int -> string
     1.5  
     1.6    (*strings*)
     1.7 +  val nth_elem_string: int * string -> string
     1.8    val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
     1.9 +  val exists_string: (string -> bool) -> string -> bool
    1.10    val enclose: string -> string -> string -> string
    1.11    val quote: string -> string
    1.12    val space_implode: string -> string list -> string
    1.13 @@ -653,13 +655,19 @@
    1.14  
    1.15  (** strings **)
    1.16  
    1.17 -(*tuned version of foldl for strings, avoids explode*)
    1.18 +(*functions tuned for strings, avoiding explode*)
    1.19 +
    1.20 +fun nth_elem_string (i, str) =
    1.21 +  String.substring (str, i, 1) handle _ => raise LIST "nth_elem_string";
    1.22 +
    1.23  fun foldl_string f (x0, str) =
    1.24    let
    1.25      val n = size str;
    1.26      fun fold (x, i) = if i < n then fold (f (x, String.substring (str, i, 1)), i + 1) else x
    1.27    in fold (x0, 0) end;
    1.28  
    1.29 +fun exists_string pred str = foldl_string (fn (b, s) => b orelse pred s) (false, str);
    1.30 +
    1.31  (*enclose in brackets*)
    1.32  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    1.33