From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 15:21:04 +0000 (+0000) Subject: added "/list_servers" method (actually used by the getter panel) X-Git-Tag: before_refactoring~38 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b93fd4b7d0835fd5b35ad5615f6b8b105a827280;p=helm.git added "/list_servers" method (actually used by the getter panel) --- diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index d8526afa9..501b9d839 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -386,6 +386,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 "\n%s\n

" + (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