From b8c0504c5602b08443cec0782670bd4a699cbc23 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 25 Jul 2005 10:15:04 +0000
Subject: [PATCH] added split

---
 helm/matita/matitaMisc.ml  | 12 ++++++++++++
 helm/matita/matitaMisc.mli |  3 +++
 2 files changed, 15 insertions(+)

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 *)
-- 
2.39.2