X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=0792d30b52a8a58ada989efe6570d3f01ab30dcd;hb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;hp=d8526afa99d61f453a1087d08020b9c7260b5ba0;hpb=a4520a0d408ece8a4e3cc1dab3f89e91f01f623d;p=helm.git
diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index d8526afa9..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 *)
@@ -386,6 +391,15 @@ let callback (req: Http_types.request) outchan =
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 ""
+ (String.concat "\n"
+ (List.map
+ (let i = ref ~-1 in
+ fun s -> incr i; sprintf "| %d | %s |
" !i s)
+ !Http_getter_env.servers)))
+ outchan
| "/add_server" ->
let name = req#param "url" in
(try