saves to gzip

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 922cc7b9a80bb069cac15a1eca1d4cbbc8d181c0..96145fa7505ea27a09bdea694b0914fd49856be8 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -287,21 +287,22 @@ let save_object_to_disk uri obj =
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
   let bodyuri = UriManager.bodyuri_of_uri uri in
   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri innertypesuri) ^ ".xml" in
+        (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
   let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in
   let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
-        (UriManager.string_of_uri uri) ^ ".xml" in
+        (UriManager.string_of_uri uri) ^ ".xml.gz" in
   let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in
   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
-        (UriManager.string_of_uri uri) ^ ".body.xml" in
+        (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
   let xmlbodypath = !(Lazy.force basedir) ^ "/" ^  xmlbodyfilename in
   let path_scheme_of path = "file://" ^ path in
   MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]);
    (* now write to disk *)
     ensure_path_exists innertypespath;
-    Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
+    Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
     ensure_path_exists xmlpath;
-    Xml.pp ~quiet:true xml (Some xmlpath) ;
+    Xml.pp ~gzip:true xml (Some xmlpath) ;
+    
    (* now register to the getter *)
     Http_getter.register' innertypesuri (path_scheme_of innertypespath); 
     Http_getter.register' uri (path_scheme_of xmlpath);
@@ -310,7 +311,7 @@ let save_object_to_disk uri obj =
        None,None -> ()
      | Some bodyxml,Some bodyuri->
          ensure_path_exists xmlbodypath;
-         Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
+         Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
          Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
      | _-> assert false)