]> matita.cs.unibo.it Git - helm.git/blobdiff - daemons/http_getter/main.ml
examples of applyS
[helm.git] / daemons / http_getter / main.ml
index 3117a85c991eed1be6c3cf81d14d2048cfe45683..572e9de1b932419203400a630186111002fec218 100644 (file)
@@ -191,10 +191,10 @@ let return_ls regexp fmt outchan =
 
 let return_help outchan = return_html_raw (Http_getter.help ()) outchan
 
-let return_resolve uri outchan =
+let return_resolve writable uri outchan =
   try
     return_xml_raw
-      (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve uri))
+      (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve ~writable uri))
       outchan
   with
   | Unresolvable_URI _ -> return_xml_raw "<unresolvable />\n" outchan
@@ -263,7 +263,7 @@ let respond_xslt patch_xslt xslt_name outchan =
 
   (* thread action *)
 
-let callback (req: Http_types.request) outchan =
+let callback ((req: Http_types.request), outchan) =
   try
     Http_getter_logger.log ("Connection from " ^ req#clientAddr);
     Http_getter_logger.log ("Received request: " ^ req#uri);
@@ -272,7 +272,8 @@ let callback (req: Http_types.request) outchan =
     | "/getxml" ->
         let uri = req#param "uri" in
         let fname = Http_getter.getxml uri in (* local name, in cache *)
-        let remote_name = Http_getter.resolve uri in (* remote name *)
+        (* remote name *)
+        let remote_name = Http_getter.resolve ~writable:false uri in 
         let src_enc = if is_gzip fname then `Gzipped else `Normal in
         let enc = parse_enc req in
         let fname, cleanup = convert_file ~from_enc:src_enc ~to_enc:enc fname in
@@ -293,7 +294,13 @@ let callback (req: Http_types.request) outchan =
     | "/getdtd" ->
         let fname = Http_getter.getdtd (req#param "uri") in
         respond_dtd (parse_patch req) fname outchan
-    | "/resolve" -> return_resolve (req#param "uri") outchan
+    | "/resolve" -> 
+        let writable = 
+          match req#param ~default:"false" "writable" with
+          | "true" -> true
+          | _ -> false
+        in
+        return_resolve writable (req#param "uri") outchan
     | "/clean_cache" ->
         Http_getter.clean_cache ();
         return_html_msg "Done." outchan
@@ -327,6 +334,11 @@ let callback (req: Http_types.request) outchan =
           log_failure msg;
           return_html_error ("uncaught_exception", msg) msg outchan)
 
+let callback req outchan =
+  HExtlib.finally
+    (fun () -> try close_out outchan with Sys_error _ -> ())
+    callback (req, outchan)
+
 let batch_update = ref false      
 
 let args = [ ]