X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=e3aadd5b5a616d143c17dd22ab71d25f7ac06626;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=1ebe49e39c2e442a1b6a922373c5efe24ba93c74;hpb=c90e354dfd2a81f03664ca68504e0932f670fe17;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 1ebe49e39..e3aadd5b5 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 0o755
+        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
@@ -232,25 +247,6 @@ 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
-    let dir = "mkdir -p " ^ d in 
-    (match Unix.system dir with
-    | Unix.WEXITED 0 -> ()
-    | Unix.WEXITED n -> 
-        MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n);
-        failwith errmsg
-    | Unix.WSIGNALED s 
-    | Unix.WSTOPPED s -> 
-        MatitaLog.error 
-          ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s);
-        failwith errmsg)
-  with Unix.Unix_error _ as exc -> 
-    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
@@ -295,8 +291,9 @@ let obj_file_of_baseuri baseuri =
   path ^ ".moo"
 
 let obj_file_of_script f =
- let baseuri = baseuri_of_file f in
-  obj_file_of_baseuri baseuri
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   obj_file_of_baseuri baseuri
 
 let rec list_uniq = function 
   | [] -> []