X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fmain.ml;h=47784d137ba4ba51d84b43bf747b14fd124177b8;hb=e8680015a9f4da6e50d9e1baa5affb9075445894;hp=8fa671ab9febd8ae04b44c687cca723f40505aee;hpb=81814dffe8a7bdc7e537b36742dcea44a51fd8ad;p=helm.git

diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml
index 8fa671ab9..47784d137 100644
--- a/helm/http_getter/main.ml
+++ b/helm/http_getter/main.ml
@@ -69,26 +69,6 @@ let parse_output_format meth (req: Http_types.request) =
   | s when String.lowercase s = "xml" -> `Xml
   | s -> raise (Bad_request ("Invalid /" ^ meth ^ " format: " ^ s))
 
-  (* parse "baseuri" format for /ls method, no default value *)
-let parse_ls_uri =
-  let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
-  let trailing_slash_RE = Pcre.regexp "/+$" in
-  let wrong_uri uri =
-    raise (Bad_request ("Invalid /ls baseuri: " ^ uri))
-  in
-  fun (req: Http_types.request) ->
-    let baseuri = req#param "baseuri" in
-    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
-
   (* parse "position" argument, default is 0 *)
 let parse_position (req: Http_types.request) =
   try
@@ -164,8 +144,8 @@ let return_all_xml_uris fmt outchan =
 let return_all_rdf_uris classs outchan =
   return_all_foo_uris "allrdfuris" (Http_getter.getallrdfuris classs) outchan
 
-let return_ls xmluri fmt outchan =
-  let ls_items = Http_getter.ls xmluri in
+let return_ls regexp fmt outchan =
+  let ls_items = Http_getter.ls regexp in
   let buf = Buffer.create 10240 in
   (match fmt with
   | `Text ->
@@ -214,8 +194,9 @@ let return_resolve uri outchan =
     return_xml_raw
       (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve uri))
       outchan
-  with Unresolvable_URI uri ->
-    return_xml_raw "<unresolved />\n" outchan
+  with
+  | Unresolvable_URI _ -> return_xml_raw "<unresolvable />\n" outchan
+  | Key_not_found _ -> return_xml_raw "<not_found />\n" outchan
 
 let return_list_servers outchan =
   return_html_raw
@@ -274,6 +255,9 @@ let callback (req: Http_types.request) outchan =
     | "/register" ->
         Http_getter.register ~uri:(req#param "uri") ~url:(req#param "url");
         return_html_msg "Register done" outchan
+    | "/unregister" ->
+        Http_getter.unregister (req#param "uri");
+        return_html_msg "Unregister done" outchan
     | "/clean_cache" ->
         Http_getter.clean_cache ();
         return_html_msg "Done." outchan
@@ -303,7 +287,7 @@ let callback (req: Http_types.request) outchan =
        return_all_xml_uris (parse_output_format "getalluris" req) outchan
     | "/getallrdfuris" -> return_all_rdf_uris (parse_rdf_class req) outchan
     | "/ls" ->
-       return_ls (parse_ls_uri req) (parse_output_format "ls" req) outchan
+        return_ls (req#param "baseuri") (parse_output_format "ls" req) outchan
     | "/getempty" ->
         Http_daemon.respond ~body:Http_getter_const.empty_xml outchan
     | invalid_request ->