(*
- * Copyright (C) 2003:
+ * Copyright (C) 2003-2004:
* Stefano Zacchiroli <zack@cs.unibo.it>
* for the HELM Team http://helm.cs.unibo.it/
*
let resource_type_of_url = function
| url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> Enc_gzipped
| url when Pcre.pmatch ~pat:"\\.xml$" url -> Enc_normal
- | url -> raise (Http_getter_invalid_URL url)
+ | url -> raise (Invalid_URL url)
let extension_of_resource_type = function
| Enc_normal -> "xml"
| Enc_gzipped -> "xml.gz"
let resource_type = resource_type_of_url url in
let extension = extension_of_resource_type resource_type in
let downloadname =
- match http_getter_uri_of_string uri with (* parse uri *)
+ match uri_of_string uri with (* parse uri *)
| Cic_uri (Cic baseuri) | Cic_uri (Theory baseuri) ->
(* assumption: baseuri starts with "/" *)
sprintf "%s%s.%s" Http_getter_env.cic_dir baseuri extension
in
let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
let contype = "text/xml" in
- (* File cache if needed and return a short circuit file.
- Short circuit is needed in situation like:
+ (* Fill cache if needed and return a short circuit file.
+ Short circuit is needed in situations like:
resource type = normal, cache type = gzipped, required encoding = normal
we would like to avoid normal -> gzipped -> normal conversions. To avoid
this tmp_short_circuit is used to remember the name of the intermediate