From: Stefano Zacchiroli Date: Mon, 25 Jul 2005 10:15:04 +0000 (+0000) Subject: added split X-Git-Tag: V_0_7_2~91 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8c0504c5602b08443cec0782670bd4a699cbc23;p=helm.git added split --- diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index c12a14527..3ed1f001c 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -118,6 +118,18 @@ let strip_trailing_blanks = let rex = Pcre.regexp "\\s*$" in fun s -> Pcre.replace ~rex s +let split ?(char = ' ') s = + let pieces = ref [] in + let rec aux idx = + match (try Some (String.index_from s idx char) with Not_found -> None) with + | Some pos -> + pieces := String.sub s idx (pos - idx) :: !pieces; + aux (pos + 1) + | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces + in + aux 0; + List.rev !pieces + let empty_mathml () = DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 86c11249a..dafd91387 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -54,6 +54,9 @@ val append_phrase_sep: string -> string val strip_trailing_blanks: string -> string val strip_trailing_slash: string -> string + (* split a string at character, char defaults to ' ' *) +val split: ?char:char -> string -> string list + val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *) (** @raise Failure *)