X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fgetter.ml;h=d3da5a579da24f566d5f26eace108518226cfd61;hb=2540cc551ae097178c7e11ec578b58977a35bd3b;hp=21c1901a183722c4b2ac040964827f7353c4e06f;hpb=c01d2aaea05f7385bee46addd900cd0397756389;p=helm.git diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml index 21c1901a1..d3da5a579 100644 --- a/helm/interface/getter.ml +++ b/helm/interface/getter.ml @@ -20,7 +20,7 @@ module MapOfStrings = Map.Make(OrderedStrings);; let read_index url = let module C = Configuration in - if Sys.command ("wget -c -P " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^ + if Sys.command ("./mywget " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^ C.indexname ^ "\"") <> 0 then raise (ErrorGetting url) ; @@ -56,6 +56,8 @@ let rec mk_urls_of_uris = uris map ;; +exception PerlGetterNotResponding;; + let update () = let module C = Configuration in let fd = open_in C.servers_file in @@ -72,7 +74,11 @@ let update () = Dbm.opendbm C.uris_dbm [Dbm.Dbm_wronly ; Dbm.Dbm_create] 0o660 in MapOfStrings.iter (fun uri url -> Dbm.add dbm uri url) urls_of_uris ; - Dbm.close dbm + Dbm.close dbm ; + (* Inform also the Perl-getter *) + if Sys.command ("wget -O /dev/null http://localhost:8081/update") <> 0 + then + raise PerlGetterNotResponding ; ;; (* url_of_uri : uri -> url *) @@ -102,7 +108,7 @@ let get_file uri = begin let url = url_of_uri uri in (*CSC: use -q for quiet mode *) - if Sys.command ("wget -c -P " ^ dir ^ " \"" ^ url ^"\"") <> 0 + if Sys.command ("./mywget " ^ dir ^ " \"" ^ url ^"\"") <> 0 then raise (ErrorGetting url) ; end ; @@ -115,8 +121,8 @@ let get uri = let module U = UriManager in get_file (U.uri_of_string - (Str.replace_first (Str.regexp "\.ann$") "" - (Str.replace_first (Str.regexp "\.types$") "" (U.string_of_uri uri)))) + (Str.replace_first (Str.regexp "\.types$") "" + (Str.replace_first (Str.regexp "\.ann$") "" (U.string_of_uri uri)))) ;; (* get_ann : uri -> filename *)