X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fgetter%2Fhttp_getter_misc.ml;h=b25a425805ad9c6a29cda92c83cd87aff2af496d;hb=f693e2de79c1a95422a5efd22acbcea5003eeaba;hp=eeea891602bf979404fe3c55a2abed7c87565cba;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/getter/http_getter_misc.ml b/helm/ocaml/getter/http_getter_misc.ml
index eeea89160..b25a42580 100644
--- a/helm/ocaml/getter/http_getter_misc.ml
+++ b/helm/ocaml/getter/http_getter_misc.ml
@@ -28,13 +28,22 @@
 
 open Printf
 
+let file_scheme_prefix = "file://"
+
 let trailing_dot_gz_RE = Pcre.regexp "\\.gz$"   (* for g{,un}zip *)
 let url_RE = Pcre.regexp "^([\\w.-]+)(:(\\d+))?(/.*)?$"
 let http_scheme_RE = Pcre.regexp ~flags:[`CASELESS] "^http://"
-let file_scheme_RE = Pcre.regexp ~flags:[`CASELESS] "^file://"
+let file_scheme_RE = Pcre.regexp ~flags:[`CASELESS] ("^" ^ file_scheme_prefix)
 let dir_sep_RE = Pcre.regexp "/"
 let heading_slash_RE = Pcre.regexp "^/"
 
+let local_url =
+  let rex = Pcre.regexp ("^(" ^ file_scheme_prefix ^ ")(.*)(.gz)$") in
+  fun s ->
+    try
+      Some ((Pcre.extract ~rex s).(2))
+    with Not_found -> None
+
 let bufsiz = 16384  (* for file system I/O *)
 let tcp_bufsiz = 4096 (* for TCP I/O *)
 
@@ -154,7 +163,6 @@ let gunzip ?(keep = false) ?output fname =
   begin
     try
       let ic = Gzip.open_in_chan zic in
-      Http_getter_logger.log (sprintf "LUCA: OK" );
       let oc = open_out output in
       let buf = String.create bufsiz in
       (try