(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) (* 24/01/2000 *) (* *) (******************************************************************************) (*CSC: il getter _DEVE_ diventare un semplice "binding" a quello in Perl *) let update () = (* deliver update request to http_getter *) ClientHTTP.send (Configuration.getter_url ^ "update") ;; (* 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 ;; let raw_get = ClientHTTP.get_and_save (* 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 raw_get (Configuration.getter_url ^ "getxml?uri=" ^ UriManager.string_of_uri uri ^ "&format=normal&patch_dtd=no" ) fn 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 "\.types$") "" (Str.replace_first (Str.regexp "\.ann$") "" (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) ;;