# HG changeset patch
# User wenzelm
# Date 1117729788 -7200
# Node ID 841342a7c41c7ff14b7b5929b981f7bf846d8828
# Parent  6ec757011ad6b99bf23a58e221fe66bd57007028
replaced foldl_string by fold_string;
added forall_string;
improved unsuffix/unprefix: no explode;

diff -r 6ec757011ad6 -r 841342a7c41c src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jun 02 18:29:47 2005 +0200
+++ b/src/Pure/library.ML	Thu Jun 02 18:29:48 2005 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/library.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Markus Wenzel, TU Munich
+    Author:     Markus Wenzel, TU Muenchen
 
 Basic library: functions, options, pairs, booleans, lists, integers,
 rational numbers, strings, lists as sets, association lists, generic
@@ -132,7 +132,6 @@
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
   val string_of_indexname: string * int -> string
-    (* CB: note alternative Syntax.string_of_vname has nicer syntax *)
   val read_radixint: int * string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string
@@ -151,8 +150,9 @@
 
   (*strings*)
   val nth_elem_string: int * string -> string
-  val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
+  val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   val exists_string: (string -> bool) -> string -> bool
+  val forall_string: (string -> bool) -> string -> bool
   val enclose: string -> string -> string -> string
   val unenclose: string -> string
   val quote: string -> string
@@ -736,19 +736,19 @@
 
 (** strings **)
 
-(*functions tuned for strings, avoiding explode*)
+(* functions tuned for strings, avoiding explode *)
 
 fun nth_elem_string (i, str) =
   (case try String.substring (str, i, 1) of
     SOME s => s
   | NONE => raise Subscript);
 
-fun foldl_string f (x0, str) =
+fun fold_string f str x0 =
   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 iter (x, i) =
+      if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x;
+  in iter (x0, 0) end;
 
 fun exists_string pred str =
   let
@@ -756,6 +756,8 @@
     fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
   in ex 0 end;
 
+fun forall_string pred = not o exists_string (not o pred);
+
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;
 fun unenclose str = String.substring (str, 1, size str - 2);
@@ -787,7 +789,6 @@
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
 
-(*untabify*)
 fun untabify chs =
   let
     val tab_width = 8;
@@ -801,25 +802,17 @@
     else flat (#2 (foldl_map untab (0, chs)))
   end;
 
-(*append suffix*)
-fun suffix sfx s = s ^ sfx;
+fun suffix sffx s = s ^ sffx;
 
-(*remove suffix*)
-fun unsuffix sfx s =
-  let
-    val cs = explode s;
-    val prfx_len = size s - size sfx;
-  in
-    if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
-      implode (take (prfx_len, cs))
+fun unsuffix sffx s =
+  let val m = size sffx; val n = size s - m in
+    if n >= 0 andalso String.substring (s, n, m) = sffx then String.substring (s, 0, n)
     else raise Fail "unsuffix"
   end;
 
-(*remove prefix*)
 fun unprefix prfx s =
-  let val (prfx', sfx) = splitAt (size prfx, explode s)
-  in
-    if implode prfx' = prfx then implode sfx
+  let val m = size prfx; val n = size s - m in
+    if String.isPrefix prfx s then String.substring (s, m, n)
     else raise Fail "unprefix"
   end;