X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FpxpUriResolver.ml;h=1be7355c759f05539a14d563be88bb57ad37ae77;hb=4ef40e8fb4de63f9699268b389f052007bc87f54;hp=7ca78aa933e360175e58fe4b3ab51e32197abf13;hpb=4faf0e37e7019de16dd6862bb34d84f799a2a230;p=helm.git diff --git a/helm/interface/pxpUriResolver.ml b/helm/interface/pxpUriResolver.ml index 7ca78aa93..1be7355c7 100644 --- a/helm/interface/pxpUriResolver.ml +++ b/helm/interface/pxpUriResolver.ml @@ -33,17 +33,15 @@ (* *) (******************************************************************************) -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 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 url_syntax =