- added support for "formatted" log messages, mainly

[helm.git] / helm / http_getter / http_getter.ml

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 5a84455a14c2c0d5e581ac4f230c3bca53ab82cc..26b0774a49bc76fdb343486612173ae4919a1222 100644 (file)
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -244,10 +244,11 @@ let return_ls =
           ~body outchan
 in
 let (index_line_sep_RE, index_sep_RE, trailing_types_RE,
-    heading_cic_RE, heading_theory_RE,
+    heading_cic_RE, heading_theory_RE, heading_nuprl_RE,
     heading_rdf_cic_RE, heading_rdf_theory_RE) =
-  (Pcre.regexp "[ \t]+", Pcre.regexp "\n+", Pcre.regexp "\\.types$",
-  Pcre.regexp "^cic:", Pcre.regexp "^theory:",
+  (Pcre.regexp "[ \t]+", Pcre.regexp "\r\n|\r|\n",
+  Pcre.regexp "\\.types$",
+  Pcre.regexp "^cic:", Pcre.regexp "^theory:", Pcre.regexp "^nuprl:",
   Pcre.regexp "^helm:rdf.*//cic:", Pcre.regexp "^helm:rdf.*//theory:")
 in
 let update_from_server logmsg server_url = (* use global maps *)
@@ -258,6 +259,8 @@ let update_from_server logmsg server_url = (* use global maps *)
         Pcre.replace ~rex:heading_cic_RE ~templ:server_url uri
     | uri when (Pcre.pmatch ~rex:heading_theory_RE uri) ->
         Pcre.replace ~rex:heading_theory_RE ~templ:server_url uri
+    | uri when (Pcre.pmatch ~rex:heading_nuprl_RE uri) ->
+        Pcre.replace ~rex:heading_nuprl_RE ~templ:server_url uri
     | uri -> raise (Http_getter_invalid_URI uri)
   in
   let rdf_url_of_uri = function (* TODO as above *)
@@ -280,19 +283,22 @@ let update_from_server logmsg server_url = (* use global maps *)
   | Some xml_index ->
       (log := !log ^ "Updating XML db ...<br />\n";
       List.iter
-        (fun l ->
-          try
-            (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")
-            | [uri] ->
-               assert (is_cic_uri uri || is_nuprl_uri uri) ;
-               (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml")
-            | _ -> log := !log ^ "Ignoring invalid line: " ^ l ^ "<br />\n")
-          with Http_getter_invalid_URI uri ->
-            log := !log ^ "Ignoring invalid XML URI: " ^ uri ^ "<br />\n")
-        (Pcre.split ~rex:index_sep_RE xml_index)) (* xml_index lines *)
+        (function
+          | l when is_blank_line l -> ()  (* skip blank and commented lines *)
+          | l ->
+              try
+                (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")
+                | [uri] ->
+                   assert (is_cic_uri uri || is_nuprl_uri uri) ;
+                   (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml")
+                | _ ->
+                    log := !log ^ "Ignoring invalid line: '" ^ l ^ "'<br />\n")
+              with Http_getter_invalid_URI uri ->
+                log := !log ^ "Ignoring invalid XML URI: '" ^ uri ^ "'<br />\n")
+            (Pcre.split ~rex:index_sep_RE xml_index)) (* xml_index lines *)
   | None -> ());
   (match rdf_index with
   | Some rdf_index ->
@@ -327,7 +333,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
@@ -415,7 +424,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;