From: Stefano Zacchiroli <zack@upsilon.cc>
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 "<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