(******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) (* 24/01/2000 *) (* *) (******************************************************************************) exception ErrorGetting of string;; module OrderedStrings = struct type t = string let compare (s1 : t) (s2 : t) = compare s1 s2 end ;; module MapOfStrings = Map.Make(OrderedStrings);; let read_index url = let module C = Configuration in if Sys.command ("wget -c -P " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^ C.indexname ^ "\"") <> 0 then raise (ErrorGetting url) ; let tmpfilename = C.tmpdir ^ "/" ^ C.indexname in let fd = open_in tmpfilename in let uris = ref [] in try while true do uris := (input_line fd) :: !uris done ; [] (* only to make the compiler happy *) with End_of_file -> Sys.remove tmpfilename ; !uris ;; (* mk_urls_of_uris list_of_servers_base_urls *) let rec mk_urls_of_uris = function [] -> MapOfStrings.empty | 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' = 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) uris map ;; let update () = let module C = Configuration in let fd = open_in C.servers_file in let servers = ref [] in try while true do servers := (input_line fd) :: !servers done with End_of_file -> let urls_of_uris = mk_urls_of_uris (List.rev !servers) in (try Sys.remove (C.uris_dbm ^ ".db") with _ -> ()) ; let dbm = 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 ;; (* url_of_uri : uri -> url *) let url_of_uri uri = let dbm = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0o660 in let url = Dbm.find dbm (UriManager.string_of_uri uri) in Dbm.close dbm ; url ;; let filedir_of_uri uri = let fn = UriManager.buri_of_uri uri in let fn' = Str.replace_first (Str.regexp ".*:") Configuration.dest fn in fn' ;; let name_and_ext_of_uri uri = let str = UriManager.string_of_uri uri in Str.replace_first (Str.regexp ".*/") "" str ;; (* get_file : uri -> filename *) let get_file uri = let dir = filedir_of_uri uri in let fn = dir ^ "/" ^ name_and_ext_of_uri uri ^ ".xml" in if not (Sys.file_exists fn) then begin let url = url_of_uri uri in (*CSC: use -q for quiet mode *) if Sys.command ("wget -c -P " ^ dir ^ " \"" ^ url ^"\"") <> 0 then raise (ErrorGetting url) ; end ; fn ;; (* get : uri -> filename *) (* If uri is the URI of an annotation, the annotated object is processed *) 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)))) ;; (* get_ann : uri -> filename *) (* If uri is the URI of an annotation, the annotation file is processed *) let get_ann = get_file;; (* get_ann_file_name_and_uri : uri -> filename * annuri *) (* If given an URI, it returns the name of the corresponding *) (* annotation file and the annotation uri *) let get_ann_file_name_and_uri uri = let module U = UriManager in let uri = U.string_of_uri uri in let annuri = U.uri_of_string ( if Str.string_match (Str.regexp ".*\.ann$") uri 0 then uri else uri ^ ".ann" ) in let dir = filedir_of_uri annuri in let fn = dir ^ "/" ^ name_and_ext_of_uri annuri ^ ".xml" in (fn, annuri) ;;