X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_misc.ml;fp=helm%2Fhttp_getter%2Fhttp_getter_misc.ml;h=0790d9415f8b4f8b68131f29afee75e967a7de12;hb=bbb280d199ff7b34f7ec00f632bfada722fd1037;hp=d1c221f35b1e52e75b27aa13b0f9b2ddda3b6fb8;hpb=866249edf202e4fec2c0e3fffdee96782009d6f3;p=helm.git

diff --git a/helm/http_getter/http_getter_misc.ml b/helm/http_getter/http_getter_misc.ml
index d1c221f35..0790d9415 100644
--- a/helm/http_getter/http_getter_misc.ml
+++ b/helm/http_getter/http_getter_misc.ml
@@ -77,32 +77,35 @@ let wget ?output url =
   end else  (* other URL, pass it to wget *)
     use_wget ()
 
-  (* stderr shown as usual *)
+let bufsiz = 16384
 let gzip ?(keep = false) fname =
-  if keep then begin  (* keep original file *)
-    debug_print ("gzip -f -c " ^ fname);
-    Shell.call
-      ~stdout:(Shell.to_file (fname ^ ".gz"))
-      [Shell.cmd "gzip" ["-f"; "-c"; fname]]
-  end else begin  (* don't keep original file *)
-    debug_print ("gzip -f " ^ fname);
-    Shell.call [Shell.cmd "gzip" ["-f"; fname]]
-  end
+  let (ic, oc) = (open_in fname, Gzip.open_out (fname ^ ".gz")) in
+  let buf = String.create bufsiz in
+  (try
+    while true do
+      let bytes = input ic buf 0 bufsiz in
+      if bytes = 0 then raise End_of_file else Gzip.output oc buf 0 bytes
+    done
+  with End_of_file -> ());
+  close_in ic;
+  Gzip.close_out oc;
+  if not keep then Sys.remove fname
 
-  (* stderr shown as usual *)
+let trailing_dot_gz_RE = Pcre.regexp "\\.gz$"
 let gunzip ?(keep = false) fname =
-  if not (Pcre.pmatch ~pat:"\\.gz$" fname) then
-    failwith "gunzip: source file doesn't end with '.gz'";
-  let basename = Pcre.replace ~pat:"\\.gz$" fname in
-  if keep then begin  (* keep original file *)
-    debug_print ("gunzip -f -c " ^ fname);
-    Shell.call
-      ~stdout:(Shell.to_file basename)
-      [Shell.cmd "gunzip" ["-f"; "-c"; fname]]
-  end else begin  (* don't keep original file *)
-    debug_print ("gunzip -f " ^ fname);
-    Shell.call [Shell.cmd "gunzip" ["-f"; fname]]
-  end
+  let basename = Pcre.replace ~rex:trailing_dot_gz_RE fname in
+  assert (basename <> fname);
+  let (ic, oc) = (Gzip.open_in fname, open_out basename) in
+  let buf = String.create bufsiz in
+  (try
+    while true do
+      let bytes = Gzip.input ic buf 0 bufsiz in
+      if bytes = 0 then raise End_of_file else output oc buf 0 bytes
+    done
+  with End_of_file -> ());
+  Gzip.close_in ic;
+  close_out oc;
+  if not keep then Sys.remove fname
 
 let tempfile () =
   let buf = Buffer.create 28 in (* strlen("/tmp/fileSzb3Mw_http_getter") *)