Added support for NuPRL URIs.

Note: theory files are supported only for CIC. To be understood.

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 7c5fafa114a5cc5831dc83782f174d04cfa346d6..40f38dc4eec38598258f23e0fbb4a3f817689af0 100644 (file)
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -79,13 +79,16 @@ let parse_ls_uri =
 
   (* global maps, shared by all threads *)
 
-let xml_map = new Http_getter_map.map Http_getter_env.xml_dbm in
+let cic_map = new Http_getter_map.map Http_getter_env.cic_dbm in
+let nuprl_map = new Http_getter_map.map Http_getter_env.nuprl_dbm in
 let rdf_map = new Http_getter_map.map Http_getter_env.rdf_dbm in
 let xsl_map = new Http_getter_map.map Http_getter_env.xsl_dbm in
 
-let save_maps () = xml_map#close; rdf_map#close; xsl_map#close in
+let save_maps () =
+ cic_map#close; nuprl_map#close; rdf_map#close; xsl_map#close in
 let map_of_uri = function
-  | uri when is_xml_uri uri -> xml_map
+  | uri when is_cic_uri uri -> cic_map
+  | uri when is_nuprl_uri uri -> nuprl_map
   | uri when is_rdf_uri uri -> rdf_map
   | uri when is_xsl_uri uri -> xsl_map
   | uri -> raise (Http_getter_unresolvable_URI uri)
@@ -123,7 +126,7 @@ let return_all_foo_uris map doctype filter outchan =
         output_string outchan (sprintf "\t<uri value=\"%s\" />\n" uri));
   output_string outchan (sprintf "</%s>\n" doctype)
 in
-let return_all_xml_uris = return_all_foo_uris xml_map "alluris" in
+let return_all_xml_uris = return_all_foo_uris cic_map "alluris" in
 let return_all_rdf_uris = return_all_foo_uris rdf_map "allrdfuris" in
 let return_ls =
   let (++) (oldann, oldtypes, oldbody) (newann, newtypes, newbody) =
@@ -171,7 +174,7 @@ let return_ls =
       in
       Hashtbl.replace objs basepart (oldflags ++ newflags)
     in
-    xml_map#iter  (* BLEARGH Dbm module lacks support for fold-like functions *)
+    cic_map#iter  (* BLEARGH Dbm module lacks support for fold-like functions *)
       (fun key _ ->
         match key with
         | uri when Pcre.pmatch ~rex:dir_RE uri ->  (* directory hit *)
@@ -274,8 +277,12 @@ let update_from_server logmsg server_url = (* use global maps *)
         (fun l ->
           try
             (match Pcre.split ~rex:index_line_sep_RE l with
-            | [uri; "gz"] -> xml_map#add uri ((xml_url_of_uri uri) ^ ".xml.gz")
-            | [uri] -> xml_map#add uri ((xml_url_of_uri uri) ^ ".xml")
+            | [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")
@@ -350,7 +357,7 @@ let callback (req: Http_types.request) outchan =
         | _ -> assert false)
     | "/update" ->
         (Http_getter_env.reload (); (* reload servers list from servers file *)
-        xml_map#clear; rdf_map#clear; xsl_map#clear;
+        cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
         let log =
           List.fold_left
             update_from_server
@@ -358,7 +365,7 @@ let callback (req: Http_types.request) outchan =
               (* reverse order: 1st server is the most important one *)
             (List.rev !Http_getter_env.servers)
         in
-        xml_map#sync; rdf_map#sync; xsl_map#sync;
+        cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync;
         return_html_msg log outchan)
     | "/getalluris" ->
         return_all_xml_uris

diff --git a/helm/http_getter/http_getter_cache.ml b/helm/http_getter/http_getter_cache.ml
index d132b69a56b2297e6508a0193cf893ace027fd99..88db99e5b6b6d1dfddc70957b0d641c8b035526b 100644 (file)
--- a/helm/http_getter/http_getter_cache.ml
+++ b/helm/http_getter/http_getter_cache.ml
@@ -65,9 +65,12 @@ let respond_xml ?(enc = Enc_normal) ?(patch = true) ~url ~uri outchan =
   let extension = extension_of_resource_type resource_type in
   let downloadname =
     match http_getter_uri_of_string uri with  (* parse uri *)
-    | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) ->
+    | Cic_uri (Cic baseuri) | Cic_uri (Theory baseuri) ->
           (* assumption: baseuri starts with "/" *)
-        sprintf "%s%s.%s" Http_getter_env.xml_dir baseuri extension
+        sprintf "%s%s.%s" Http_getter_env.cic_dir baseuri extension
+    | Nuprl_uri baseuri ->
+          (* assumption: baseuri starts with "/" *)
+        sprintf "%s%s.%s" Http_getter_env.nuprl_dir baseuri extension
     | Rdf_uri (prefix, ((Cic baseuri) as qbaseuri))
     | Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) ->
         let escaped_prefix =

diff --git a/helm/http_getter/http_getter_common.ml b/helm/http_getter/http_getter_common.ml
index b7cbc936c57a17fa21e1f72366b975960e2ed7de..40e5648ca2379ece56bbd69acdb025fff3f3b303 100644 (file)
--- a/helm/http_getter/http_getter_common.ml
+++ b/helm/http_getter/http_getter_common.ml
@@ -34,9 +34,10 @@ let string_of_encoding = function
   | Enc_normal -> "Normal"
   | Enc_gzipped -> "GZipped"
 
-let is_cic_uri uri = Pcre.pmatch ~pat:"^cic:" uri
+let is_cic_obj_uri uri = Pcre.pmatch ~pat:"^cic:" uri
 let is_theory_uri uri = Pcre.pmatch ~pat:"^theory:" uri
-let is_xml_uri uri = is_cic_uri uri || is_theory_uri uri
+let is_cic_uri uri = is_cic_obj_uri uri || is_theory_uri uri
+let is_nuprl_uri uri = Pcre.pmatch ~pat:"^nuprl:" uri
 let is_rdf_uri uri = Pcre.pmatch ~pat:"^helm:rdf(.*):(.*)//(.*)" uri
 let is_xsl_uri uri = Pcre.pmatch ~pat:"^\\w+\\.xsl" uri
 
@@ -46,14 +47,15 @@ let rec http_getter_uri_of_string = function
       | [ prefix; uri ] ->
           let rest =
             match http_getter_uri_of_string uri with
-            | Xml_uri xmluri -> xmluri
+            | Cic_uri xmluri -> xmluri
             | _ -> raise (Http_getter_invalid_URI uri)
           in
           Rdf_uri (prefix, rest)
       | _ -> raise (Http_getter_invalid_URI uri))
-  | uri when is_cic_uri uri -> Xml_uri (Cic (Pcre.replace ~pat:"^cic:" uri))
+  | uri when is_cic_uri uri -> Cic_uri (Cic (Pcre.replace ~pat:"^cic:" uri))
+  | uri when is_nuprl_uri uri -> Nuprl_uri (Pcre.replace ~pat:"^nuprl:" uri)
   | uri when is_theory_uri uri ->
-      Xml_uri (Theory (Pcre.replace ~pat:"^theory:" uri))
+      Cic_uri (Theory (Pcre.replace ~pat:"^theory:" uri))
   | uri -> raise (Http_getter_invalid_URI uri)
 
 let patch_xml line =

diff --git a/helm/http_getter/http_getter_common.mli b/helm/http_getter/http_getter_common.mli
index 9ac5aad6fde50b9cd801f140af6f247cf53a1a07..05f495f2f6efeb107355ae43ef847b36d8b75913 100644 (file)
--- a/helm/http_getter/http_getter_common.mli
+++ b/helm/http_getter/http_getter_common.mli
@@ -31,7 +31,8 @@ open Http_getter_types;;
 val string_of_ls_flag: http_getter_ls_flag -> string
 val string_of_encoding: http_getter_encoding -> string
 
-val is_xml_uri: string -> bool
+val is_cic_uri: string -> bool
+val is_nuprl_uri: string -> bool
 val is_rdf_uri: string -> bool
 val is_xsl_uri: string -> bool
 

diff --git a/helm/http_getter/http_getter_env.ml b/helm/http_getter/http_getter_env.ml
index 217ec346ee39c2c80c414eb5b0fdbf40f400972c..35cd5bbd937dd6f350c7788ee7be0788557f3a69 100644 (file)
--- a/helm/http_getter/http_getter_env.ml
+++ b/helm/http_getter/http_getter_env.ml
@@ -83,13 +83,15 @@ let parse_servers () =
 let servers = ref (parse_servers ())
 let reload_servers () = servers := parse_servers ()
 
-let xml_dbm = safe_getenv "HTTP_GETTER_XML_DBM"
+let cic_dbm = safe_getenv "HTTP_GETTER_CIC_DBM"
+let nuprl_dbm = safe_getenv "HTTP_GETTER_NUPRL_DBM"
 let rdf_dbm = safe_getenv "HTTP_GETTER_RDF_DBM"
 let xsl_dbm = safe_getenv "HTTP_GETTER_XSL_DBM"
 let xml_index = safe_getenv "HTTP_GETTER_XML_INDEXNAME"
 let rdf_index = safe_getenv "HTTP_GETTER_RDF_INDEXNAME"
 let xsl_index = safe_getenv "HTTP_GETTER_XSL_INDEXNAME"
-let xml_dir = safe_getenv "HTTP_GETTER_XML_DIR"
+let cic_dir = safe_getenv "HTTP_GETTER_CIC_DIR"
+let nuprl_dir = safe_getenv "HTTP_GETTER_NUPRL_DIR"
 let rdf_dir = safe_getenv "HTTP_GETTER_RDF_DIR"
 let dtd_dir = safe_getenv "HTTP_GETTER_DTD_DIR"
 
@@ -123,13 +125,15 @@ let dump_env () =
   printf
 "HTTP Getter %s (the OCaml one!)
 
-xml_dbm:\t%s
+cic_dbm:\t%s
+nuprl_dbm:\t%s
 rdf_dbm:\t%s
 xsl_dbm:\t%s
 xml_index:\t%s
 rdf_index:\t%s
 xsl_index:\t%s
-xml_dir:\t%s
+cic_dir:\t%s
+nuprl_dir:\t%s
 rdf_dir:\t%s
 dtd_dir:\t%s
 servers_file:\t%s
@@ -143,8 +147,9 @@ conf_dir:\t%s
 servers:
 \t%s
 "
-    version xml_dbm rdf_dbm xsl_dbm xml_index rdf_index xsl_index
-    xml_dir rdf_dir dtd_dir servers_file host port my_own_url dtd_base_url
+    version cic_dbm nuprl_dbm rdf_dbm xsl_dbm xml_index rdf_index xsl_index
+    cic_dir nuprl_dir rdf_dir dtd_dir servers_file host port my_own_url
+    dtd_base_url
     (match cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped")
     conf_file conf_dir (String.concat "\n\t" !servers);
   flush stdout

diff --git a/helm/http_getter/http_getter_env.mli b/helm/http_getter/http_getter_env.mli
index 2f71d5735c59c55083908df706e0ae8737ec0121..eab0e79d2b7d37abeb9388568d6a741a46325b1b 100644 (file)
--- a/helm/http_getter/http_getter_env.mli
+++ b/helm/http_getter/http_getter_env.mli
@@ -34,13 +34,15 @@ val version       : string        (* getter version *)
 
   (* environment gathered data *)
 
-val xml_dbm       : string        (* XML map DBM file *)
+val cic_dbm       : string        (* XML map DBM file for CIC *)
+val nuprl_dbm     : string        (* XML map DBM file for NuPRL *)
 val rdf_dbm       : string        (* RDF map DBM file *)
 val xsl_dbm       : string        (* XSL map DBM file *)
 val xml_index     : string        (* XMLs' index *)
 val rdf_index     : string        (* RDFs' index *)
 val xsl_index     : string        (* XSLTs' index *)
-val xml_dir       : string        (* XMLs' directory *)
+val cic_dir       : string        (* XMLs' directory  for CIC*)
+val nuprl_dir     : string        (* XMLs' directory for NuPRL*)
 val rdf_dir       : string        (* RDFs' directory *)
 val dtd_dir       : string        (* DTDs' root directory *)
 val servers_file  : string        (* servers.txt file *)

diff --git a/helm/http_getter/http_getter_types.ml b/helm/http_getter/http_getter_types.ml
index b54a2ef06b1ba5294bc3ba0ff728c2c4f1dba2aa..01af4faec0ef0030375c54d4171df986c14cd2ab 100644 (file)
--- a/helm/http_getter/http_getter_types.ml
+++ b/helm/http_getter/http_getter_types.ml
@@ -41,8 +41,10 @@ type http_getter_xml_uri =
   | Cic of string
   | Theory of string
 type http_getter_rdf_uri = string * http_getter_xml_uri
+type http_getter_nuprl_uri = string
 type http_getter_uri =
-  | Xml_uri of http_getter_xml_uri
+  | Cic_uri of http_getter_xml_uri
+  | Nuprl_uri of http_getter_nuprl_uri
   | Rdf_uri of http_getter_rdf_uri
 
 module StringSet = Set.Make (String)