(*
- * Copyright (C) 2003, HELM Team.
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
*)
+(* TODO cache expires control!!! *)
+(* TODO possible race condition, e.g.:
+ two clients require the same URI which is available in cache compressed, the
+ getter need to uncompress it, send back to client, and delete the
+ uncompressed file. Actually the uncompressed file name is the same, a temp
+ file isn't used. *)
+(* TODO possible race condition, e.g.:
+ two clients require the same URI which is not available in cache, cache
+ filling operation can collide *)
+(* TODO uwobo loop:
+ if two large proof (already in cache) are requested at the same time by two
+ clients, uwobo (java implementation, not yet tested with the OCaml one)
+ starts looping sending output to one of the client *)
+
open Http_getter_common;;
open Http_getter_misc;;
open Http_getter_types;;
let extension = extension_of_resource_type resource_type in
let downloadname =
match http_getter_uri_of_string uri with (* parse uri *)
- | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) ->
+ | Cic_uri (Cic baseuri) | Cic_uri (Theory baseuri) ->
+ (* assumption: baseuri starts with "/" *)
+ sprintf "%s%s.%s" Http_getter_env.cic_dir baseuri extension
+ | Nuprl_uri baseuri ->
(* assumption: baseuri starts with "/" *)
- sprintf "%s%s.%s" Http_getter_env.xml_dir baseuri extension
+ sprintf "%s%s.%s" Http_getter_env.nuprl_dir baseuri extension
| Rdf_uri (prefix, ((Cic baseuri) as qbaseuri))
| Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) ->
let escaped_prefix =