]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: a4520a0)
added "/list_servers" method (actually used by the getter panel)
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 15:21:04 +0000 (15:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 15:21:04 +0000 (15:21 +0000)
helm/http_getter/http_getter.ml patch | blob | history

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index d8526afa99d61f453a1087d08020b9c7260b5ba0..501b9d8390dd8692488a0d095ed87adeffd92077 100644 (file)
--- 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
Unnamed repository; edit this file 'description' to name the repository.