added split

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c12a1452733208ca2f3ab755bf727587a344ab42..3ed1f001c2d17f5c2b185362b71f1fd0f0e443a8 100644 (file)
--- 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 86c11249aaf26465949bf8eefaf15d2bbaf4eb68..dafd91387a8dee473897e6d0b71d127316635284 100644 (file)
--- 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 *)