- added support for NuPRL URIs in xml_url_of_uri

- added support for blank and #-commented lines in indexes
- added support for index lines terminated both with \r and \r\n

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 5a84455a14c2c0d5e581ac4f230c3bca53ab82cc..b5cfa47d9564561c09783dfb85b702ae280f7605 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 ->