string primtives
authorpaulson
Fri Dec 22 20:58:14 2006 +0100 (2006-12-22)
changeset 21899dab16d14db60
parent 21898 46be40d304d7
child 21900 f386d7eb17d1
string primtives
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Dec 22 15:35:17 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Dec 22 20:58:14 2006 +0100
     1.3 @@ -163,6 +163,7 @@
     1.4    val unsuffix: string -> string -> string
     1.5    val replicate_string: int -> string -> string
     1.6    val translate_string: (string -> string) -> string -> string
     1.7 +  val nospaces: string -> string
     1.8  
     1.9    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.10    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.11 @@ -770,13 +771,7 @@
    1.12  
    1.13  (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
    1.14  fun space_explode _ "" = []
    1.15 -  | space_explode sep str =
    1.16 -      let
    1.17 -        fun expl chs =
    1.18 -          (case take_prefix (fn s => s <> sep) chs of
    1.19 -            (cs, []) => [implode cs]
    1.20 -          | (cs, _ :: cs') => implode cs :: expl cs');
    1.21 -      in expl (explode str) end;
    1.22 +  | space_explode sep s = String.fields (fn c => str c = sep) s;
    1.23  
    1.24  val split_lines = space_explode "\n";
    1.25  
    1.26 @@ -813,6 +808,7 @@
    1.27        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    1.28        else replicate_string (k div 2) (a ^ a) ^ a;
    1.29  
    1.30 +val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
    1.31  
    1.32  
    1.33  (** lists as sets -- see also Pure/General/ord_list.ML **)