1.1 --- a/src/Pure/library.ML	Thu Jun 02 18:29:47 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Jun 02 18:29:48 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/library.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Author:     Markus Wenzel, TU Munich
     1.8 +    Author:     Markus Wenzel, TU Muenchen
     1.9  
    1.10  Basic library: functions, options, pairs, booleans, lists, integers,
    1.11  rational numbers, strings, lists as sets, association lists, generic
    1.12 @@ -132,7 +132,6 @@
    1.13    val radixstring: int * string * int -> string
    1.14    val string_of_int: int -> string
    1.15    val string_of_indexname: string * int -> string
    1.16 -    (* CB: note alternative Syntax.string_of_vname has nicer syntax *)
    1.17    val read_radixint: int * string list -> int * string list
    1.18    val read_int: string list -> int * string list
    1.19    val oct_char: string -> string
    1.20 @@ -151,8 +150,9 @@
    1.21  
    1.22    (*strings*)
    1.23    val nth_elem_string: int * string -> string
    1.24 -  val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
    1.25 +  val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
    1.26    val exists_string: (string -> bool) -> string -> bool
    1.27 +  val forall_string: (string -> bool) -> string -> bool
    1.28    val enclose: string -> string -> string -> string
    1.29    val unenclose: string -> string
    1.30    val quote: string -> string
    1.31 @@ -736,19 +736,19 @@
    1.32  
    1.33  (** strings **)
    1.34  
    1.35 -(*functions tuned for strings, avoiding explode*)
    1.36 +(* functions tuned for strings, avoiding explode *)
    1.37  
    1.38  fun nth_elem_string (i, str) =
    1.39    (case try String.substring (str, i, 1) of
    1.40      SOME s => s
    1.41    | NONE => raise Subscript);
    1.42  
    1.43 -fun foldl_string f (x0, str) =
    1.44 +fun fold_string f str x0 =
    1.45    let
    1.46      val n = size str;
    1.47 -    fun fold (x, i) =
    1.48 -      if i < n then fold (f (x, String.substring (str, i, 1)), i + 1) else x;
    1.49 -  in fold (x0, 0) end;
    1.50 +    fun iter (x, i) =
    1.51 +      if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x;
    1.52 +  in iter (x0, 0) end;
    1.53  
    1.54  fun exists_string pred str =
    1.55    let
    1.56 @@ -756,6 +756,8 @@
    1.57      fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
    1.58    in ex 0 end;
    1.59  
    1.60 +fun forall_string pred = not o exists_string (not o pred);
    1.61 +
    1.62  (*enclose in brackets*)
    1.63  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    1.64  fun unenclose str = String.substring (str, 1, size str - 2);
    1.65 @@ -787,7 +789,6 @@
    1.66  fun prefix_lines "" txt = txt
    1.67    | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
    1.68  
    1.69 -(*untabify*)
    1.70  fun untabify chs =
    1.71    let
    1.72      val tab_width = 8;
    1.73 @@ -801,25 +802,17 @@
    1.74      else flat (#2 (foldl_map untab (0, chs)))
    1.75    end;
    1.76  
    1.77 -(*append suffix*)
    1.78 -fun suffix sfx s = s ^ sfx;
    1.79 +fun suffix sffx s = s ^ sffx;
    1.80  
    1.81 -(*remove suffix*)
    1.82 -fun unsuffix sfx s =
    1.83 -  let
    1.84 -    val cs = explode s;
    1.85 -    val prfx_len = size s - size sfx;
    1.86 -  in
    1.87 -    if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
    1.88 -      implode (take (prfx_len, cs))
    1.89 +fun unsuffix sffx s =
    1.90 +  let val m = size sffx; val n = size s - m in
    1.91 +    if n >= 0 andalso String.substring (s, n, m) = sffx then String.substring (s, 0, n)
    1.92      else raise Fail "unsuffix"
    1.93    end;
    1.94  
    1.95 -(*remove prefix*)
    1.96  fun unprefix prfx s =
    1.97 -  let val (prfx', sfx) = splitAt (size prfx, explode s)
    1.98 -  in
    1.99 -    if implode prfx' = prfx then implode sfx
   1.100 +  let val m = size prfx; val n = size s - m in
   1.101 +    if String.isPrefix prfx s then String.substring (s, m, n)
   1.102      else raise Fail "unprefix"
   1.103    end;
   1.104