]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.ml
clean_cache method added
[helm.git] / helm / http_getter / http_getter.ml
index d8526afa99d61f453a1087d08020b9c7260b5ba0..48c82f8eaae356ba2f7f5218c35600b4dc1720b0 100644 (file)
@@ -71,16 +71,21 @@ let parse_output_format (req: Http_types.request) =
 let parse_ls_uri =
   let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/+$" in
+  let wrong_uri uri =
+    raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ uri))
+  in
   fun (req: Http_types.request) ->
     let baseuri = req#param "baseuri" in
-    let subs =
-      Pcre.extract ~rex:parse_ls_RE
-        (Pcre.replace ~rex:trailing_slash_RE  baseuri)
-    in
-    match (subs.(1), subs.(2)) with
-    | "cic", uri -> Cic uri
-    | "theory", uri -> Theory uri
-    | _ -> raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ baseuri))
+    try
+      let subs =
+        Pcre.extract ~rex:parse_ls_RE
+          (Pcre.replace ~rex:trailing_slash_RE  baseuri)
+      in
+      (match (subs.(1), subs.(2)) with
+      | "cic", uri -> Cic uri
+      | "theory", uri -> Theory uri
+      | _ -> wrong_uri baseuri)
+    with Not_found -> wrong_uri baseuri
 ;;
 
   (* global maps, shared by all threads *)
@@ -382,10 +387,22 @@ let callback (req: Http_types.request) outchan =
             register uri url;
             return_html_msg "Register done" outchan
         | _ -> assert false)
+    | "/clean_cache" ->
+        Http_getter_cache.clean ();
+        return_html_msg "Done." outchan
     | "/update" ->
         Http_getter_env.reload (); (* reload servers list from servers file *)
         let log = update_from_all_servers () in
         return_html_msg log outchan
+    | "/list_servers" ->
+        return_html_raw
+          (sprintf "<html><body><table>\n%s\n</table></body></html>"
+            (String.concat "\n"
+              (List.map
+                (let i = ref ~-1 in
+                fun s -> incr i; sprintf "<tr><td>%d</td><td>%s</td></tr>" !i s)
+                !Http_getter_env.servers)))
+          outchan
     | "/add_server" ->
         let name = req#param "url" in
         (try