matitaprover

[helm.git] / helm / software / components / library / librarySync.ml

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index a59294aaa73f7eb3173b1d6047809f27061fee76..338e84bbe4d2294617d050e4ab35c417efd276ad 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -59,6 +59,12 @@ let paths_and_uris_of_obj uri =
   xmlunivgraphpath, univgraphuri
 
 let save_object_to_disk uri obj ugraph univlist =
+  let write f x =
+    if not (Helm_registry.get_opt_default 
+              Helm_registry.bool "matita.nodisk" ~default:false) 
+    then      
+      f x
+  in
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     HExtlib.mkdir dir
@@ -74,11 +80,11 @@ let save_object_to_disk uri obj ugraph univlist =
       xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri 
   in
-  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+  write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
-  ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath);
-  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
+  write ensure_path_exists xmlpath;
+  write (Xml.pp ~gzip:true xml) (Some xmlpath);
+  write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
@@ -86,8 +92,8 @@ let save_object_to_disk uri obj ugraph univlist =
     (match bodyxml,bodyuri with
        None,_ -> []
      | Some bodyxml,Some bodyuri->
-         ensure_path_exists xmlbodypath;
-         Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+         write ensure_path_exists xmlbodypath;
+         write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
          [bodyuri, xmlbodypath]
      | _-> assert false)