X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=0792d30b52a8a58ada989efe6570d3f01ab30dcd;hb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;hp=b5cfa47d9564561c09783dfb85b702ae280f7605;hpb=2779c4191d0c14aa7bec9a861974a6a1f815ca03;p=helm.git

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index b5cfa47d9..0792d30b5 100644
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -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 *)
@@ -105,7 +110,10 @@ let resolve uri =
   with Http_getter_map.Key_not_found _ ->
     raise (Http_getter_unresolvable_URI uri)
 in
-let register uri =  (map_of_uri uri )#add uri in
+let register uri =
+  (* Warning: this fail if uri is already registered *)
+  (map_of_uri uri)#add uri
+in
 let return_all_foo_uris map doctype filter outchan =
   (** return all URIs contained in 'map' which satisfy predicate 'filter'; URIs
   are written in an XMLish format ('doctype' is the XML doctype) onto 'outchan'
@@ -290,10 +298,12 @@ let update_from_server logmsg server_url = (* use global maps *)
                 (match Pcre.split ~rex:index_line_sep_RE l with
                 | [uri; "gz"] ->
                    assert (is_cic_uri uri || is_nuprl_uri uri) ;
-                   (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml.gz")
+                   (map_of_uri uri)#replace
+                    uri ((xml_url_of_uri uri) ^ ".xml.gz")
                 | [uri] ->
                    assert (is_cic_uri uri || is_nuprl_uri uri) ;
-                   (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml")
+                   (map_of_uri uri)#replace
+                    uri ((xml_url_of_uri uri) ^ ".xml")
                 | _ ->
                     log := !log ^ "Ignoring invalid line: '" ^ l ^ "'<br />\n")
               with Http_getter_invalid_URI uri ->
@@ -307,8 +317,9 @@ let update_from_server logmsg server_url = (* use global maps *)
         (fun l ->
           try
             (match Pcre.split ~rex:index_line_sep_RE l with
-            | [uri; "gz"] -> rdf_map#add uri ((rdf_url_of_uri uri) ^ ".xml.gz")
-            | [uri] -> rdf_map#add uri ((rdf_url_of_uri uri) ^ ".xml")
+            | [uri; "gz"] ->
+                rdf_map#replace uri ((rdf_url_of_uri uri) ^ ".xml.gz")
+            | [uri] -> rdf_map#replace uri ((rdf_url_of_uri uri) ^ ".xml")
             | _ -> log := !log ^ "Ignoring invalid line: " ^ l ^ "<br />\n")
           with Http_getter_invalid_URI uri ->
             log := !log ^ "Ignoring invalid RDF URI: " ^ uri ^ "<br />\n")
@@ -318,13 +329,25 @@ let update_from_server logmsg server_url = (* use global maps *)
   | Some xsl_index ->
       (log := !log ^ "Updating XSLT db ...<br />\n";
       List.iter
-        (fun l -> xsl_map#add l (server_url ^ "/" ^ l))
+        (fun l -> xsl_map#replace l (server_url ^ "/" ^ l))
         (Pcre.split ~rex:index_sep_RE xsl_index);
       log := !log ^ "All done!<br />\n")
   | None -> ());
   debug_print "done with this server";
   !log
 in
+let update_from_all_servers () =  (* use global maps *)
+  cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
+  let log =
+    List.fold_left
+      update_from_server
+      ""  (* initial logmsg: empty *)
+        (* reverse order: 1st server is the most important one *)
+      (List.rev !Http_getter_env.servers)
+  in
+  cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync;
+  log
+in
 
   (* thread action *)
 
@@ -333,7 +356,10 @@ let callback (req: Http_types.request) outchan =
     debug_print ("Connection from " ^ req#clientAddr);
     debug_print ("Received request: " ^ req#path);
     (match req#path with
-    | "/help" -> return_html_raw Http_getter_const.usage_string outchan
+    | "/help" ->
+        return_html_raw
+          (Http_getter_const.usage_string (Http_getter_env.env_to_string ()))
+          outchan
     | "/getxml" | "/getxslt" | "/getdtd" | "/resolve" | "/register" ->
         (let uri = req#param "uri" in  (* common parameter *)
         match req#path with
@@ -362,17 +388,74 @@ let callback (req: Http_types.request) outchan =
             return_html_msg "Register done" outchan
         | _ -> assert false)
     | "/update" ->
-        (Http_getter_env.reload (); (* reload servers list from servers file *)
-        cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
-        let log =
-          List.fold_left
-            update_from_server
-            ""  (* initial logmsg: empty *)
-              (* reverse order: 1st server is the most important one *)
-            (List.rev !Http_getter_env.servers)
+        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
+          let position =
+            try
+              let res = int_of_string (req#param "position") in
+              if res < 0 then
+                raise (Failure "int_of_string");
+              res
+            with Failure "int_of_string" ->
+              raise (Http_getter_bad_request
+                (sprintf "position must be a non negative integer (%s given)"
+                  (req#param "position")))
+          in
+          if position = 0 then  (* fallback to default value *)
+            raise (Http_types.Param_not_found "foo")
+          else if position > 0 then begin (* add server and update all *)
+            Http_getter_env.add_server ~position name;
+            let log = update_from_all_servers () in
+            return_html_msg
+              (sprintf "Added server %s in position %d)<br />\n%s"
+                name position log)
+              outchan
+          end else (* position < 0 *) (* error! *)
+            assert false (* already checked above *)
+        with Http_types.Param_not_found _ ->  (* add as 1st server by default *)
+          Http_getter_env.add_server ~position:0 name;
+          let log = update_from_server  (* quick update (new server only) *)
+            (sprintf "Added server %s in head position<br />\n" name) name
+          in
+          return_html_msg log outchan)
+    | "/remove_server" ->
+        let position =
+          try
+            let res = int_of_string (req#param "position") in
+            if res < 0 then
+              raise (Failure "int_of_string");
+            res
+          with Failure "int_of_string" ->
+            raise (Http_getter_bad_request
+              (sprintf "position must be a non negative integer (%s given)"
+                (req#param "position")))
         in
-        cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync;
-        return_html_msg log outchan)
+        let server_name =
+          try
+            List.nth !Http_getter_env.servers position
+          with Failure "nth" ->
+            raise (Http_getter_bad_request
+              (sprintf "no server with position %d" position))
+        in
+        Http_getter_env.remove_server position;
+        let log = update_from_all_servers () in
+        return_html_msg
+          (sprintf "Removed server %s (position %d)<br />\n%s"
+            server_name position log)
+          outchan
     | "/getalluris" ->
         return_all_xml_uris
           (fun uri ->
@@ -421,7 +504,8 @@ in
     (* daemon initialization *)
 
 let main () =
-  Http_getter_env.dump_env ();
+  print_string (Http_getter_env.env_to_string ());
+  flush stdout;
   Unix.putenv "http_proxy" "";
   at_exit save_maps;
   Sys.catch_break true;