From: Stefano Zacchiroli Date: Fri, 3 Feb 2006 15:15:33 +0000 (+0000) Subject: made "dtd_dir" optional, is needed only by the web server, not by matita X-Git-Tag: make_still_working~7650 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b67ea513f11d1ef3d9fd228c64913561424662e2;p=helm.git made "dtd_dir" optional, is needed only by the web server, not by matita --- diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 61930a4aa..1b47a6c38 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -176,7 +176,7 @@ let getdtd uri = if remote () then getdtd_remote uri else begin - let fname = Lazy.force Http_getter_env.dtd_dir ^ "/" ^ uri in + let fname = Http_getter_env.get_dtd_dir () ^ "/" ^ uri in if not (Sys.file_exists fname) then raise (Dtd_not_found uri); fname end diff --git a/helm/ocaml/getter/http_getter_common.ml b/helm/ocaml/getter/http_getter_common.ml index a29a44de2..ddce33f5d 100644 --- a/helm/ocaml/getter/http_getter_common.ml +++ b/helm/ocaml/getter/http_getter_common.ml @@ -84,8 +84,7 @@ let patch_system kind ?(via_http = true) () = sprintf "%s $1 SYSTEM \"%s/getdtd?uri=" kind (Lazy.force Http_getter_env.my_own_url) else - sprintf "%s $1 SYSTEM \"file://%s/" kind - (Lazy.force Http_getter_env.dtd_dir) + sprintf "%s $1 SYSTEM \"file://%s/" kind (Http_getter_env.get_dtd_dir ()) in fun line -> Pcre.replace ~rex ~templ line diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml index 7a3891b98..79b0ab42e 100644 --- a/helm/ocaml/getter/http_getter_env.ml +++ b/helm/ocaml/getter/http_getter_env.ml @@ -38,7 +38,10 @@ let version = Http_getter_const.version let prefix_RE = Pcre.regexp "^\\s*([^\\s]+)\\s+([^\\s]+)\\s*(.*)$" let cache_dir = lazy (normalize_dir (Helm_registry.get "getter.cache_dir")) -let dtd_dir = lazy (normalize_dir (Helm_registry.get "getter.dtd_dir")) +let dtd_dir = lazy ( + match Helm_registry.get_opt Helm_registry.get_string "getter.dtd_dir" with + | None -> None + | Some dir -> Some (normalize_dir dir)) let dtd_base_urls = lazy ( let rex = Pcre.regexp "/*$" in let raw_urls = @@ -107,8 +110,14 @@ log_level:\t%d " version (pp_prefixes (Lazy.force prefixes)) - (Lazy.force dtd_dir) (Lazy.force host) (Lazy.force port) + (match Lazy.force dtd_dir with Some dir -> dir | None -> "NONE") + (Lazy.force host) (Lazy.force port) (Lazy.force my_own_url) (String.concat " " (Lazy.force dtd_base_urls)) (match Http_getter_logger.get_log_file () with None -> "None" | Some f -> f) (Http_getter_logger.get_log_level ()) +let get_dtd_dir () = + match Lazy.force dtd_dir with + | None -> raise (Internal_error "dtd_dir is not available") + | Some dtd_dir -> dtd_dir + diff --git a/helm/ocaml/getter/http_getter_env.mli b/helm/ocaml/getter/http_getter_env.mli index 6a0f0f50a..d1ab73db8 100644 --- a/helm/ocaml/getter/http_getter_env.mli +++ b/helm/ocaml/getter/http_getter_env.mli @@ -33,7 +33,7 @@ val version : string (* getter version *) (** all *_dir values are returned with trailing "/" *) val cache_dir : string lazy_t (* cache root *) -val dtd_dir : string lazy_t (* DTDs' root directory *) +val dtd_dir : string option lazy_t (* DTDs' root directory *) val port : int lazy_t (* port on which getter listens *) val dtd_base_urls : string list lazy_t (* base URLs for document patching *) val prefixes : (string * (string * prefix_attr list)) list lazy_t @@ -50,3 +50,5 @@ val env_to_string : unit -> string (* dump a textual representation of the current http_getter settings on an output channel *) +val get_dtd_dir : unit -> string +