From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 27 Jul 2005 12:26:52 +0000 (+0000)
Subject: safe mkdir implemented
X-Git-Tag: V_0_7_2~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f37481ee495d25d2e0a0feb1cdf6e443d3e4530c;p=helm.git

safe mkdir implemented
---

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 1ebe49e39..9ddc268a8 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -114,6 +114,21 @@ let append_phrase_sep s =
   else
     s
 
+let mkdir path =
+  let components = Str.split (Str.regexp "/") path in
+  let rec aux where = function
+    | [] -> ()
+    | piece::tl -> 
+        let path = where ^ "/" ^ piece in
+        (try
+          Unix.mkdir path 755
+        with 
+        | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
+        | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
+        aux path tl
+  in
+  aux "" components
+
 let strip_trailing_blanks =
   let rex = Pcre.regexp "\\s*$" in
   fun s -> Pcre.replace ~rex s
@@ -231,7 +246,7 @@ class ['a] browser_history ?memento size init =
 let singleton f =
   let instance = lazy (f ()) in
   fun () -> Lazy.force instance
-
+(*
 let mkdir d =
   let errmsg = sprintf "Unable to create directory \"%s\"" d in
   try
@@ -250,7 +265,7 @@ let mkdir d =
     MatitaLog.error 
       ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc));
     failwith errmsg
-
+*)
 let get_proof_status status =
   match status.proof_status with
   | Incomplete_proof s -> s