X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=88e44ea7a017012ab8387f692743a238e516e696;hb=541a200b13431987114dd3fd88ec9764cee1e772;hp=640b7406ee17f925832f864d410f7e95fb5b233c;hpb=7deafec4fd4b2eebf4d4061f21ee5c47bd15b062;p=helm.git

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 640b7406e..88e44ea7a 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -256,6 +256,21 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
 let 
  save_object_to_disk uri obj 
 =
+  let ensure_path_exists path =
+    let dir = Filename.dirname path in
+    try 
+      let stats = Unix.stat dir in
+      if stats.Unix.st_kind <> Unix.S_DIR then
+        raise (Failure (dir ^ " already exists and is not a directory"))
+      else
+        ()
+    with
+      Unix.Unix_error (_,_,_) -> 
+        let pstatus = Unix.system ("mkdir -p " ^ dir) in
+        match pstatus with
+        | Unix.WEXITED n when n = 0 -> ()
+        | _ -> raise (Failure ("Unable to create " ^ dir))
+  in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
@@ -286,7 +301,9 @@ let
   let path_scheme_of path = "file:/" ^ path in
 
    (* now write to disk *)
+    ensure_path_exists innertypespath;
     Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
+    ensure_path_exists xmlpath;
     Xml.pp ~quiet:true xml (Some xmlpath) ;
 
    (* now register to the getter *)
@@ -297,6 +314,7 @@ let
     (match bodyxml,bodyuri with
        None,None -> ()
      | Some bodyxml,Some bodyuri->
+         ensure_path_exists xmlbodypath;
          Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
          Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
      | _-> assert false)