X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_common.ml;h=15810b93c2b4b8fb535c187eda61ae6eed1785fb;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=03f5c2a2ad19e06ff7564ba36c3d9df4b00a86d1;hpb=4cc248707314a05902ce8d70ceea1ac0541f9976;p=helm.git diff --git a/helm/ocaml/getter/http_getter_common.ml b/helm/ocaml/getter/http_getter_common.ml index 03f5c2a2a..15810b93c 100644 --- a/helm/ocaml/getter/http_getter_common.ml +++ b/helm/ocaml/getter/http_getter_common.ml @@ -52,7 +52,7 @@ let rec uri_of_string = function in Rdf_uri (prefix, rest) | _ -> raise (Invalid_URI uri)) - | uri when is_cic_uri uri -> Cic_uri (Cic (Pcre.replace ~pat:"^cic:" uri)) + | uri when is_cic_obj_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 -> Cic_uri (Theory (Pcre.replace ~pat:"^theory:" uri)) @@ -90,9 +90,26 @@ let patch_system kind ?(via_http = true) () = let patch_entity = patch_system "ENTITY" let patch_doctype = patch_system "DOCTYPE" +let patch_xmlbase = + let rex = Pcre.regexp "^(\\s*<\\w[^ ]*)(\\s|>)" in + fun xmlbases baseurl baseuri s -> + let s' = + Pcre.replace ~rex + ~templ:(sprintf "$1 xml:base=\"%s\" helm:base=\"%s\"$2" baseurl baseuri) + s + in + if s <> s' then xmlbases := None; + s' + let patch_dtd = patch_entity -let patch_xml ?via_http () line = - patch_doctype ?via_http () (patch_entity ?via_http () line) +let patch_xml ?via_http ?xmlbases () = + let xmlbases = ref xmlbases in + fun line -> + match !xmlbases with + | None -> patch_doctype ?via_http () (patch_entity ?via_http () line) + | Some (xmlbaseuri, xmlbaseurl) -> + patch_xmlbase xmlbases xmlbaseurl xmlbaseuri + (patch_doctype ?via_http () (patch_entity ?via_http () line)) let return_file ~fname ?contype ?contenc @@ -106,7 +123,7 @@ let return_file | (None, None) -> [] in if via_http then begin - Http_daemon.send_basic_headers ~code:200 outchan; + Http_daemon.send_basic_headers ~code:(`Code 200) outchan; Http_daemon.send_headers headers outchan; Http_daemon.send_CRLF outchan end;