From 033dc1b4f6af15fc911d2cae8a93c7c48b2feb63 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Feb 2005 16:13:28 +0000 Subject: [PATCH] saves to gzip --- helm/matita/matitaInterpreter.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 922cc7b9a..96145fa75 100644 --- 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) -- 2.39.2