exception ErrorGetting of string;;
+(* FEATURE MOVED TO HTTP_GETTER, Zack
module OrderedStrings =
struct
type t = string
let compare (s1 : t) (s2 : t) = compare s1 s2
end
;;
+*)
+
+(* FEATURE MOVED TO HTTP_GETTER, Zack
module MapOfStrings = Map.Make(OrderedStrings);;
+*)
+(* FEATURE MOVED TO HTTP_GETTER, Zack
let read_index url =
let module C = Configuration in
- if Sys.command ("helm_wget " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
+ if Sys.command ("helm_wget " ^ C.tmp_dir ^ " " ^ url ^ "/\"" ^
C.indexname ^ "\"") <> 0
then
raise (ErrorGetting url) ;
- let tmpfilename = C.tmpdir ^ "/" ^ C.indexname in
+ let tmpfilename = C.tmp_dir ^ "/" ^ C.indexname in
let fd = open_in tmpfilename in
let uris = ref [] in
try
while true do
- uris := (input_line fd) :: !uris
+ let (uri,comp) =
+ match (Str.split (Str.regexp "[ \t]+") (input_line fd)) with
+ [uri] -> (uri,"")
+ | [uri;comp] -> (uri,".gz")
+ in
+ uris := (uri,comp) :: !uris
done ;
[] (* only to make the compiler happy *)
with
Sys.remove tmpfilename ;
!uris
;;
+*)
+(* FEATURE MOVED TO HTTP_GETTER, Zack
(* mk_urls_of_uris list_of_servers_base_urls *)
let rec mk_urls_of_uris =
function
| he::tl ->
let map = mk_urls_of_uris tl in
let uris = read_index he in
- let url_of_uri uri =
- let url = uri ^ ".xml" in
+ let url_of_uri (uri,comp) =
+ let url = uri ^ ".xml" ^ comp in
let url' = Str.replace_first (Str.regexp "cic:") he url in
let url'' = Str.replace_first (Str.regexp "theory:") he url' in
url''
in
List.fold_right
- (fun uri m -> MapOfStrings.add uri (url_of_uri uri) m)
+ (fun (uri,comp) m -> MapOfStrings.add uri (url_of_uri (uri,comp)) m)
uris map
;;
+*)
exception PerlGetterNotResponding;;
+(* FEATURE MOVED TO HTTP_GETTER, Zack
let update () =
let module C = Configuration in
let fd = open_in C.servers_file in
then
raise PerlGetterNotResponding ;
;;
+*)
+
+let update () =
+(* deliver update request to http_getter *)
+ ClientHTTP.send (Configuration.getter_url ^ "update")
+;;
(* url_of_uri : uri -> url *)
let url_of_uri uri =
fn
;;
+let raw_get = ClientHTTP.get_and_save
+
(* get : uri -> filename *)
(* If uri is the URI of an annotation, the annotated object is processed *)
let get uri =