]> matita.cs.unibo.it Git - helm.git/commitdiff
renamed clientHTTP to http_getter_wget
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 15 Jun 2005 13:35:49 +0000 (13:35 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 15 Jun 2005 13:35:49 +0000 (13:35 +0000)
helm/ocaml/getter/.depend
helm/ocaml/getter/Makefile
helm/ocaml/getter/clientHTTP.ml [deleted file]
helm/ocaml/getter/clientHTTP.mli [deleted file]
helm/ocaml/getter/http_getter.ml
helm/ocaml/getter/http_getter_types.ml
helm/ocaml/getter/http_getter_wget.ml [new file with mode: 0644]
helm/ocaml/getter/http_getter_wget.mli [new file with mode: 0644]

index d620a3c9a8274137d43abdee0c94d22491045b5c..141c2a88c43fd56d76f4976ed98a71a7ae5b7794 100644 (file)
@@ -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 
index 2895f12e1fb581c077ae7d88900a7025b28fa980..d90461131e51d2a3faf58764a8b25246bdc3a290 100644 (file)
@@ -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 (file)
index b4e0e26..0000000
+++ /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 (file)
index f45d63d..0000000
+++ /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
index 41d62fb380bb966d4dcacef94d99ba7a1eb18125..a4bbb1172b6ad84c454298b2f48ae9d28376eaa1 100644 (file)
@@ -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 *)
 
index e8e31bd0fdff90f9e595d1647ea40643a1f906e4..1574e2bdb12e4249a82a421602194325dbc343ae 100644 (file)
@@ -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 (file)
index 0000000..99a9f01
--- /dev/null
@@ -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 (file)
index 0000000..4c97831
--- /dev/null
@@ -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
+