From: Stefano Zacchiroli Date: Wed, 6 Jul 2005 12:58:05 +0000 (+0000) Subject: added support for multiple binding of the same prefix (needed by the X-Git-Tag: V_0_7_1~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2220ec0d80a2846eee56922c76468ad0839f6228;p=helm.git added support for multiple binding of the same prefix (needed by the getter daemon for handling stylesheets) --- diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index bddc04dd4..75e91e4c1 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -25,10 +25,10 @@ http_getter_map.cmo: http_getter_types.cmo http_getter_misc.cmi \ http_getter_map.cmx: http_getter_types.cmx http_getter_misc.cmx \ http_getter_map.cmi http_getter.cmo: http_getter_wget.cmi http_getter_types.cmo \ - http_getter_storage.cmi http_getter_misc.cmi http_getter_map.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_const.cmi \ - http_getter_common.cmi http_getter.cmi + http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ + http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ + http_getter.cmi http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_map.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_const.cmx \ - http_getter_common.cmx http_getter.cmi + http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ + http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ + http_getter.cmi diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index e0b948ad9..795148b4b 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -88,7 +88,7 @@ let getter_url () = Helm_registry.get "getter.url" (* *) let getxml_remote uri = not_implemented "getxml_remote" -let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote" +let getxslt_remote uri = not_implemented "getxslt_remote" let getdtd_remote uri = not_implemented "getdtd_remote" let clean_cache_remote () = not_implemented "clean_cache_remote" let list_servers_remote () = not_implemented "list_servers_remote" @@ -148,25 +148,16 @@ let resolve uri = with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri) let getxml uri = - if remote () then - getxml_remote uri + if remote () then getxml_remote uri else begin try Http_getter_storage.filename (uri ^ xml_suffix) with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri) end -let getxslt uri = assert false -(* let getxslt ?(patch_dtd = true) uri = - if remote () then - getxslt_remote ~patch_dtd uri - else begin - let url = resolve uri in - let (fname, outchan) = temp_file_of_uri uri in - Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan; - close_out outchan; - fname - end *) +let getxslt uri = + if remote () then getxslt_remote uri + else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri) let getdtd uri = if remote () then diff --git a/helm/ocaml/getter/http_getter_storage.ml b/helm/ocaml/getter/http_getter_storage.ml index 01a5a521e..3418956ea 100644 --- a/helm/ocaml/getter/http_getter_storage.ml +++ b/helm/ocaml/getter/http_getter_storage.ml @@ -43,6 +43,7 @@ let http_scheme_RE = Pcre.regexp "^http://" let newline_RE = Pcre.regexp "\\n" let cic_scheme_sep_RE = Pcre.regexp ":/" let gz_suffix = ".gz" +let gz_suffix_len = String.length gz_suffix let path_of_file_url url = assert (Pcre.pmatch ~rex:file_scheme_RE url); @@ -78,6 +79,16 @@ let resolve_prefix uri = | (rex, _, url_prefix) :: _ -> Pcre.replace_first ~rex ~templ:url_prefix uri | [] -> raise (Unresolvable_URI uri) +let resolve_prefixes uri = + let matches = + List.filter (fun (rex, _, _) -> Pcre.pmatch ~rex uri) + (Lazy.force prefix_map) + in + if matches = [] then raise (Unresolvable_URI uri); + List.map + (fun (rex, _, url_prefix) -> Pcre.replace_first ~rex ~templ:url_prefix uri) + matches + let exists_http _ url = Http_getter_wget.exists (url ^ gz_suffix) || Http_getter_wget.exists url @@ -95,8 +106,8 @@ let resolve_file _ fname = with Not_found -> raise Not_found' let strip_gz_suffix fname = - if extension fname = ".gz" then - String.sub fname 0 (String.length fname - 3) + if extension fname = gz_suffix then + String.sub fname 0 (String.length fname - gz_suffix_len) else fname @@ -177,15 +188,13 @@ type 'a storage_method = { http: string -> string -> 'a; (* unresolved uri, resolved uri *) } -let dispatch storage_method uri = - assert (extension uri <> ".gz"); - let uri = (* add trailing slash to roots *) - try - if uri.[String.length uri - 1] = ':' then uri ^ "/" - else uri - with Invalid_argument _ -> uri - in - let url = resolve_prefix uri in +let normalize_root uri = (* add trailing slash to roots *) + try + if uri.[String.length uri - 1] = ':' then uri ^ "/" + else uri + with Invalid_argument _ -> uri + +let invoke_method storage_method uri url = try if Pcre.pmatch ~rex:file_scheme_RE url then storage_method.file uri (path_of_file_url url) @@ -195,17 +204,40 @@ let dispatch storage_method uri = raise (Unsupported_scheme url) with Not_found' -> raise (Resource_not_found (storage_method.name, uri)) +let dispatch_single storage_method uri = + assert (extension uri <> gz_suffix); + let uri = normalize_root uri in + let url = resolve_prefix uri in + invoke_method storage_method uri url + +let dispatch_multi storage_method uri = + let urls = resolve_prefixes uri in + let rec aux = function + | [] -> raise (Resource_not_found (storage_method.name, uri)) + | url :: tl -> + (try + invoke_method storage_method uri url + with Resource_not_found _ -> aux tl) + in + aux urls + let exists = - dispatch { name = "exists"; file = exists_file; http = exists_http } + dispatch_single { name = "exists"; file = exists_file; http = exists_http } + let resolve = - dispatch { name = "resolve"; file = resolve_file; http = resolve_http } + dispatch_single { name = "resolve"; file = resolve_file; http = resolve_http } + let ls_single = - dispatch { name = "ls"; file = ls_file_single; http = ls_http_single } -let get = dispatch { name = "get"; file = get_file; http = get_http } + dispatch_single { name = "ls"; file = ls_file_single; http = ls_http_single } + let remove = - dispatch { name = "remove"; file = remove_file; http = remove_http } + dispatch_single { name = "remove"; file = remove_file; http = remove_http } -let filename = get +let filename ?(find = false) = + if find then + dispatch_multi { name = "filename"; file = get_file; http = get_http } + else + dispatch_single { name = "filename"; file = get_file; http = get_http } (* ls_single performs ls only below a single prefix, but prefixes which have * common prefix (sorry) with a given one may need to be considered as well diff --git a/helm/ocaml/getter/http_getter_storage.mli b/helm/ocaml/getter/http_getter_storage.mli index f14c3b635..5dd997843 100644 --- a/helm/ocaml/getter/http_getter_storage.mli +++ b/helm/ocaml/getter/http_getter_storage.mli @@ -53,7 +53,7 @@ val ls: string -> string list * that the search is performed only if the asked resource is not found in * cache (i.e. to perform the find again you need to clean the cache). * Defaults to false *) -val filename: (* ?find:bool -> *) string -> string +val filename: ?find:bool -> string -> string (** only works for local resources * if both compressed and non-compressed versions of a resource exist, both of diff --git a/helm/ocaml/getter/sample.conf.xml b/helm/ocaml/getter/sample.conf.xml index 52f383fec..d292dfb88 100644 --- a/helm/ocaml/getter/sample.conf.xml +++ b/helm/ocaml/getter/sample.conf.xml @@ -19,6 +19,12 @@ cic:/matita/ file:///home/zacchiro/helm/matita/.matita/xml/matita/ + theory:/ file:///projects/helm/library/theories/ @@ -33,5 +39,13 @@ http://mowgli.cs.unibo.it/~sacerdot/ida/IDA/ --> + + xslt:/ + file:///projects/helm/xml/stylesheets/ + + + xslt:/ + file:///projects/helm/xml/stylesheets_ccorn/ +