]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_cache.ml
- label name changes: s/patch_dtd/patch because "patch_dtd" isn't really
[helm.git] / helm / http_getter / http_getter_cache.ml
index 6d2fe6e06fa52ed4480c6354492e6731acec8560..8d180e1f86a18c52eeda7adac40a614583487947 100644 (file)
@@ -1,5 +1,5 @@
 (*
- *  Copyright (C) 2000, HELM Team.
+ *  Copyright (C) 2003, HELM Team.
  *
  *  This file is part of HELM, an Hypertextual, Electronic
  *  Library of Mathematics, developed at the Computer Science
@@ -25,6 +25,7 @@
  *)
 
 open Http_getter_common;;
+open Http_getter_misc;;
 open Http_getter_types;;
 open Printf;;
 
@@ -43,11 +44,11 @@ let is_in_cache basename =
     | Enc_normal -> basename
     | Enc_gzipped -> basename ^ ".gz")
 
-let respond_xml ?(enc = Enc_normal) ?(patch_dtd = true) ~url ~uri outchan =
+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
+    match http_getter_uri_of_string uri with  (* parse uri *)
     | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) ->
           (* assumption: baseuri starts with "/" *)
         sprintf "%s%s.%s" Http_getter_env.xml_dir baseuri extension
@@ -65,10 +66,11 @@ let respond_xml ?(enc = Enc_normal) ?(patch_dtd = true) ~url ~uri outchan =
           Http_getter_env.rdf_dir escaped_prefix baseuri extension
   in
   let patch_fun =
-    if patch_dtd then Http_getter_common.patch_xml else (fun x -> x)
+    if patch then Http_getter_common.patch_xml else (fun x -> x)
   in
   let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
   if not (is_in_cache basename) then begin (* download and fill cache *)
+    mkdir ~parents:true (Filename.dirname downloadname);
     wget ~output:downloadname url;
     match (resource_type, Http_getter_env.cache_mode) with
     | Enc_normal, Enc_normal ->
@@ -98,21 +100,23 @@ let respond_xml ?(enc = Enc_normal) ?(patch_dtd = true) ~url ~uri outchan =
   | Enc_gzipped, Enc_normal -> Sys.remove (basename ^ ".gz")
 
   (* TODO enc is not yet supported *)
-let respond_xsl ?(enc = Enc_normal) ?(patch_dtd = true) ~url outchan =
+let respond_xsl ?(enc = Enc_normal) ?(patch = true) ~url outchan =
   let patch_fun =
-    if patch_dtd then Http_getter_common.patch_xsl else (fun x -> x)
+    if patch then Http_getter_common.patch_xsl else (fun x -> x)
   in
   let fname = tempfile () in
   wget ~output:fname url;
   return_file ~fname ~contype:"text/xml" ~patch_fun outchan;
   Sys.remove fname
 
-  (* TODO patch_dtd and format are fooish, implement them! *)
-let respond_dtd ?(enc = Enc_normal) ?(patch_dtd = true) ~url outchan =
-    if Sys.file_exists url then
-      return_file
-        ~fname:url ~contype:"text/xml" ~patch_fun:Http_getter_common.patch_dtd
-        outchan
-    else
-      return_html_error ("Can't find DTD: " ^ url) outchan
+  (* TODO enc is not yet supported *)
+let respond_dtd ?(enc = Enc_normal) ?(patch = true) ~url outchan =
+  let patch_fun =
+    if patch then Http_getter_common.patch_dtd else (fun x -> x)
+  in
+  if Sys.file_exists url then
+    (* TODO check this: old getter here used text/xml *)
+    return_file ~fname:url ~contype:"text/plain" ~patch_fun outchan
+  else
+    return_html_error ("Can't find DTD: " ^ url) outchan