X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FpxpUriResolver.ml;h=7ca78aa933e360175e58fe4b3ab51e32197abf13;hb=caab26f85122e0040555139c48a9111a0b2b9fff;hp=1be7355c759f05539a14d563be88bb57ad37ae77;hpb=5a7ec1a3e9cea3050ad08b2f6f57c0dad2d5a632;p=helm.git diff --git a/helm/interface/pxpUriResolver.ml b/helm/interface/pxpUriResolver.ml index 1be7355c7..7ca78aa93 100644 --- a/helm/interface/pxpUriResolver.ml +++ b/helm/interface/pxpUriResolver.ml @@ -33,15 +33,17 @@ (* *) (******************************************************************************) -let resolve = - function - "http://localhost:8081/getdtd?uri=cic.dtd" -> - Configuration.dtd_dir ^ "/cic.dtd" - | "http://localhost:8081/getdtd?uri=maththeory.dtd" -> - Configuration.dtd_dir ^ "/maththeory.dtd" - | "http://localhost:8081/getdtd?uri=annotations.dtd" -> - Configuration.dtd_dir ^ "/annotations.dtd" - | s -> s +let resolve s = + let starts_with s s' = + if String.length s < String.length s' then + false + else + (String.sub s 0 (String.length s')) = s' + in + if starts_with s "http:" then + ClientHTTP.get_and_save_to_tmp s + else + s ;; let url_syntax =