Declarative tactics for rewriting steps, elimination of the existential

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a59294aaa73f7eb3173b1d6047809f27061fee76..e1b73821bc6176014ca5c55bb30474858b126f30 100644 (file)
--- a/components/library/librarySync.ml
+++ b/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) 
 
@@ -313,12 +319,13 @@ let generate_projections refinement_toolkit uri fields =
         let composites = 
          if coercion then
             begin
-              prerr_endline ("composite for " ^ UriManager.string_of_uri uri);
+(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
               let x = add_coercion ~add_composites:true refinement_toolkit uri
               in
-              prerr_endline ("are: ");
-              List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
-              prerr_endline "---";
+(*prerr_endline ("are: ");
+  List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+  prerr_endline "---";
+*)
               x
             end
           else