added split

[helm.git] / helm / matita / matitaMisc.ml

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