From: Stefano Zacchiroli Date: Wed, 15 Jun 2005 13:35:49 +0000 (+0000) Subject: renamed clientHTTP to http_getter_wget X-Git-Tag: PRE_STORAGE~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=617285cac8aabbe62699d5d7144b0df4f5771000;p=helm.git renamed clientHTTP to http_getter_wget --- diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index d620a3c9a..141c2a88c 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -4,8 +4,8 @@ http_getter_cache.cmi: http_getter_types.cmo http_getter.cmi: http_getter_types.cmo tree.cmo: tree.cmi tree.cmx: tree.cmi -clientHTTP.cmo: clientHTTP.cmi -clientHTTP.cmx: clientHTTP.cmi +http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi +http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi http_getter_logger.cmx: http_getter_logger.cmi http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi @@ -32,11 +32,11 @@ http_getter_cache.cmo: http_getter_types.cmo http_getter_misc.cmi \ http_getter_cache.cmx: http_getter_types.cmx http_getter_misc.cmx \ http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmx \ http_getter_cache.cmi -http_getter.cmo: tree.cmi http_getter_types.cmo http_getter_misc.cmi \ - http_getter_md5.cmi http_getter_map.cmi http_getter_logger.cmi \ - http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter_cache.cmi clientHTTP.cmi http_getter.cmi -http_getter.cmx: tree.cmx http_getter_types.cmx http_getter_misc.cmx \ - http_getter_md5.cmx http_getter_map.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter_cache.cmx clientHTTP.cmx http_getter.cmi +http_getter.cmo: tree.cmi http_getter_wget.cmi http_getter_types.cmo \ + http_getter_misc.cmi http_getter_md5.cmi http_getter_map.cmi \ + http_getter_logger.cmi http_getter_env.cmi http_getter_const.cmi \ + http_getter_common.cmi http_getter_cache.cmi http_getter.cmi +http_getter.cmx: tree.cmx http_getter_wget.cmx http_getter_types.cmx \ + http_getter_misc.cmx http_getter_md5.cmx http_getter_map.cmx \ + http_getter_logger.cmx http_getter_env.cmx http_getter_const.cmx \ + http_getter_common.cmx http_getter_cache.cmx http_getter.cmi diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile index 2895f12e1..d90461131 100644 --- a/helm/ocaml/getter/Makefile +++ b/helm/ocaml/getter/Makefile @@ -5,18 +5,19 @@ REQUIRES = \ http dbm pcre shell zip \ helm-xml helm-thread helm-logger helm-urimanager helm-registry -INTERFACE_FILES = \ - tree.mli \ - clientHTTP.mli \ - http_getter_logger.mli \ - http_getter_misc.mli \ - http_getter_const.mli \ - http_getter_env.mli \ - http_getter_md5.mli \ - http_getter_common.mli \ - http_getter_map.mli \ - http_getter_cache.mli \ - http_getter.mli +INTERFACE_FILES = \ + tree.mli \ + http_getter_wget.mli \ + http_getter_logger.mli \ + http_getter_misc.mli \ + http_getter_const.mli \ + http_getter_env.mli \ + http_getter_md5.mli \ + http_getter_common.mli \ + http_getter_map.mli \ + http_getter_cache.mli \ + http_getter.mli \ + $(NULL) IMPLEMENTATION_FILES = \ http_getter_types.ml \ diff --git a/helm/ocaml/getter/clientHTTP.ml b/helm/ocaml/getter/clientHTTP.ml deleted file mode 100644 index b4e0e26b6..000000000 --- a/helm/ocaml/getter/clientHTTP.ml +++ /dev/null @@ -1,63 +0,0 @@ -(* 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/. - *) - -exception HttpClientError of string * string;; (* reason, uri *) - -let send cmd = - try - ignore (Http_user_agent.get cmd) - with - e -> raise (HttpClientError (Printexc.to_string e, cmd)) -;; - -let get uri = - try - Http_user_agent.get uri - with - e -> raise (HttpClientError (Printexc.to_string e, uri)) -;; - -let get_and_save uri dest_filename = - let out_channel = open_out dest_filename in - Http_user_agent.get_iter (output_string out_channel) uri; - close_out out_channel -;; - -let get_and_save_to_tmp uri = - let flat_string s s' c = - let cs = String.copy s in - for i = 0 to (String.length s) - 1 do - if String.contains s' s.[i] then cs.[i] <- c - done ; - cs - in - let user = try Unix.getlogin () with _ -> "" in - let tmp_file = - Filename.temp_file (user ^ flat_string uri ".-=:;!?/&" '_') "" - in - get_and_save uri tmp_file ; - tmp_file -;; - diff --git a/helm/ocaml/getter/clientHTTP.mli b/helm/ocaml/getter/clientHTTP.mli deleted file mode 100644 index f45d63dda..000000000 --- a/helm/ocaml/getter/clientHTTP.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* 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/. - *) - -exception HttpClientError of string * string;; (* reason, uri *) -val send : string -> unit -val get : string -> string -val get_and_save : string -> string -> unit -val get_and_save_to_tmp : string -> string diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 41d62fb38..a4bbb1172 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -42,17 +42,18 @@ type resolve_result = type logger_callback = HelmLogger.html_tag -> unit -let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag) +let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag) let not_implemented s = raise (Not_implemented ("Http_getter." ^ s)) -let (index_line_sep_RE, index_sep_RE, trailing_types_RE, - heading_cic_RE, heading_theory_RE, heading_nuprl_RE, - heading_rdf_cic_RE, heading_rdf_theory_RE) = - (Pcre.regexp "[ \t]+", Pcre.regexp "\r\n|\r|\n", - Pcre.regexp "\\.types$", - Pcre.regexp "^cic:", Pcre.regexp "^theory:", Pcre.regexp "^nuprl:", - Pcre.regexp "^helm:rdf.*//cic:", Pcre.regexp "^helm:rdf.*//theory:") +let index_line_sep_RE = Pcre.regexp "[ \t]+" +let index_sep_RE = Pcre.regexp "\r\n|\r|\n" +let trailing_types_RE = Pcre.regexp "\\.types$" +let heading_cic_RE = Pcre.regexp "^cic:" +let heading_theory_RE = Pcre.regexp "^theory:" +let heading_nuprl_RE, = Pcre.regexp "^nuprl:" +let heading_rdf_cic_RE = Pcre.regexp "^helm:rdf.*//cic:" +let heading_rdf_theory_RE = Pcre.regexp "^helm:rdf.*//theory:" (* global maps, shared by all threads *) @@ -258,7 +259,9 @@ let ls_remote lsuri = not_implemented "ls_remote" let resolve_remote uri = (* deliver resolve request to http_getter *) - let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in + let doc = + Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) + in let res = ref Unknown in let start_element tag attrs = match tag with @@ -283,13 +286,14 @@ let resolve_remote uri = | Resolved url -> url let register_remote ~uri ~url = - ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) + Http_getter_wget.send + (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) let unregister_remote uri = - ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) + Http_getter_wget.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) let update_remote logger () = - let answer = ClientHTTP.get (getter_url () ^ "update") in + let answer = Http_getter_wget.get (getter_url () ^ "update") in logger (`T answer); logger `BR @@ -300,7 +304,7 @@ let getxml_remote ~format ~patch_dtd uri = (match format with `Normal -> "normal" | `Gzipped -> "gz") (match patch_dtd with true -> "yes" | false -> "no") in - ClientHTTP.get_and_save_to_tmp uri + Http_getter_wget.get_and_save_to_tmp uri (* API *) diff --git a/helm/ocaml/getter/http_getter_types.ml b/helm/ocaml/getter/http_getter_types.ml index e8e31bd0f..1574e2bdb 100644 --- a/helm/ocaml/getter/http_getter_types.ml +++ b/helm/ocaml/getter/http_getter_types.ml @@ -36,6 +36,7 @@ exception Cache_failure of string exception Dtd_not_found of string (* dtd's url *) exception Key_already_in of string;; exception Key_not_found of string;; +exception Http_client_error of string * string (* url, error message *) type encoding = [ `Normal | `Gzipped ] type answer_format = [ `Text | `Xml ] diff --git a/helm/ocaml/getter/http_getter_wget.ml b/helm/ocaml/getter/http_getter_wget.ml new file mode 100644 index 000000000..99a9f01e7 --- /dev/null +++ b/helm/ocaml/getter/http_getter_wget.ml @@ -0,0 +1,57 @@ +(* Copyright (C) 2000-2005, 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/. + *) + +open Http_getter_types + +let send cmd = + try + ignore (Http_user_agent.get cmd) + with e -> raise (Http_client_error (cmd, Printexc.to_string e)) + +let get uri = + try + Http_user_agent.get uri + with e -> raise (Http_client_error (Printexc.to_string e, uri)) + +let get_and_save uri dest_filename = + let out_channel = open_out dest_filename in + Http_user_agent.get_iter (output_string out_channel) uri; + close_out out_channel + +let get_and_save_to_tmp uri = + let flat_string s s' c = + let cs = String.copy s in + for i = 0 to (String.length s) - 1 do + if String.contains s' s.[i] then cs.[i] <- c + done ; + cs + in + let user = try Unix.getlogin () with _ -> "" in + let tmp_file = + Filename.temp_file (user ^ flat_string uri ".-=:;!?/&" '_') "" + in + get_and_save uri tmp_file ; + tmp_file + diff --git a/helm/ocaml/getter/http_getter_wget.mli b/helm/ocaml/getter/http_getter_wget.mli new file mode 100644 index 000000000..4c978314e --- /dev/null +++ b/helm/ocaml/getter/http_getter_wget.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2000-2005, 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/. + *) + +val send: string -> unit + +val get: string -> string +val get_and_save: string -> string -> unit +val get_and_save_to_tmp: string -> string +