]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_cache.ml
split into two major parts:
[helm.git] / helm / http_getter / http_getter_cache.ml
index b77536f0cbc30242b129c4bfdf4236dceddb3392..8f5bc231286b0976b9723975ede7a79c9b38540b 100644 (file)
@@ -1,5 +1,5 @@
 (*
- * Copyright (C) 2003:
+ * Copyright (C) 2003-2004:
  *    Stefano Zacchiroli <zack@cs.unibo.it>
  *    for the HELM Team http://helm.cs.unibo.it/
  *
@@ -52,7 +52,7 @@ let threadSafe = new threadSafe ;;
 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"
@@ -68,7 +68,7 @@ let respond_xml ?(enc = Enc_normal) ?(patch = true) ~url ~uri outchan =
   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
@@ -93,8 +93,8 @@ let respond_xml ?(enc = Enc_normal) ?(patch = true) ~url ~uri outchan =
   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