helm/interface/getter.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 24/01/2000                                 *)
  32 (*                                                                            *)
  33 (******************************************************************************)
  34
  35
  36 (*CSC: il getter _DEVE_ diventare un semplice "binding" a quello in Perl *)
  37
  38 let update () =
  39 (* deliver update request to http_getter *)
  40  ClientHTTP.send (Configuration.getter_url ^ "update")
  41 ;;
  42
  43 (* url_of_uri : uri -> url *)
  44 let url_of_uri uri =
  45  let dbm = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0o660 in
  46   let url = Dbm.find dbm (UriManager.string_of_uri uri) in
  47    Dbm.close dbm ;
  48    url
  49 ;;
  50
  51 let filedir_of_uri uri =
  52  let fn = UriManager.buri_of_uri uri in
  53   let fn' = Str.replace_first (Str.regexp ".*:") Configuration.dest fn in
  54    fn'
  55 ;;
  56
  57 let name_and_ext_of_uri uri =
  58  let str = UriManager.string_of_uri uri in
  59   Str.replace_first (Str.regexp ".*/") "" str
  60 ;;
  61
  62 let raw_get = ClientHTTP.get_and_save
  63
  64 (* get_file : uri -> filename *)
  65 let get_file uri =
  66  let dir = filedir_of_uri uri in
  67   let fn = dir ^ "/" ^ name_and_ext_of_uri uri ^ ".xml" in
  68    if not (Sys.file_exists fn) then
  69     begin
  70      let url = url_of_uri uri in
  71       raw_get
  72        (Configuration.getter_url ^ "getxml?uri=" ^
  73         UriManager.string_of_uri uri ^ "&format=normal&patch_dtd=no"
  74        ) fn
  75     end ;
  76    fn
  77 ;;
  78
  79 (* get : uri -> filename *)
  80 (* If uri is the URI of an annotation, the annotated object is processed *)
  81 let get uri =
  82  let module U = UriManager in
  83   get_file
  84    (U.uri_of_string
  85     (Str.replace_first (Str.regexp "\.types$") ""
  86      (Str.replace_first (Str.regexp "\.ann$") "" (U.string_of_uri uri))))
  87 ;;
  88
  89 (* get_ann : uri -> filename *)
  90 (* If uri is the URI of an annotation, the annotation file is processed *)
  91 let get_ann = get_file;;
  92
  93 (* get_ann_file_name_and_uri : uri -> filename * annuri *)
  94 (* If given an URI, it returns the name of the corresponding *)
  95 (* annotation file and the annotation uri                    *)
  96 let get_ann_file_name_and_uri uri =
  97  let module U = UriManager in
  98   let uri = U.string_of_uri uri in
  99    let annuri =
 100     U.uri_of_string (
 101      if Str.string_match (Str.regexp ".*\.ann$") uri 0 then
 102       uri
 103      else
 104       uri ^ ".ann"
 105     )
 106    in
 107     let dir = filedir_of_uri annuri in
 108      let fn = dir ^ "/" ^ name_and_ext_of_uri annuri ^ ".xml" in
 109       (fn, annuri)
 110 ;;