# HG changeset patch # User paulson # Date 1166817494 -3600 # Node ID dab16d14db609faafcf0f01e5a2c52172dc88814 # Parent 46be40d304d7ab5bb28578a60d42e2a5929bf889 string primtives diff -r 46be40d304d7 -r dab16d14db60 src/Pure/library.ML --- a/src/Pure/library.ML Fri Dec 22 15:35:17 2006 +0100 +++ b/src/Pure/library.ML Fri Dec 22 20:58:14 2006 +0100 @@ -163,6 +163,7 @@ val unsuffix: string -> string -> string val replicate_string: int -> string -> string val translate_string: (string -> string) -> string -> string + val nospaces: string -> string (*lists as sets -- see also Pure/General/ord_list.ML*) val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool @@ -770,13 +771,7 @@ (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) fun space_explode _ "" = [] - | space_explode sep str = - let - fun expl chs = - (case take_prefix (fn s => s <> sep) chs of - (cs, []) => [implode cs] - | (cs, _ :: cs') => implode cs :: expl cs'); - in expl (explode str) end; + | space_explode sep s = String.fields (fn c => str c = sep) s; val split_lines = space_explode "\n"; @@ -813,6 +808,7 @@ if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) else replicate_string (k div 2) (a ^ a) ^ a; +val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c); (** lists as sets -- see also Pure/General/ord_list.ML **)