From a933ca25f485ac27e662444c250b8773c73b2755 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 7 Feb 2003 12:05:57 +0000 Subject: [PATCH] Added support for NuPRL URIs. Note: theory files are supported only for CIC. To be understood. --- helm/http_getter/http_getter.ml | 25 ++++++++++++++++--------- helm/http_getter/http_getter_cache.ml | 7 +++++-- helm/http_getter/http_getter_common.ml | 12 +++++++----- helm/http_getter/http_getter_common.mli | 3 ++- helm/http_getter/http_getter_env.ml | 17 +++++++++++------ helm/http_getter/http_getter_env.mli | 6 ++++-- helm/http_getter/http_getter_types.ml | 4 +++- 7 files changed, 48 insertions(+), 26 deletions(-) diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index 7c5fafa11..40f38dc4e 100644 --- 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\n" uri)); output_string outchan (sprintf "\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 ^ "
\n") with Http_getter_invalid_URI uri -> log := !log ^ "Ignoring invalid XML URI: " ^ uri ^ "
\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 d132b69a5..88db99e5b 100644 --- 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 b7cbc936c..40e5648ca 100644 --- 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 9ac5aad6f..05f495f2f 100644 --- 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 217ec346e..35cd5bbd9 100644 --- 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 2f71d5735..eab0e79d2 100644 --- 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 b54a2ef06..01af4faec 100644 --- 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) -- 2.39.2