X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibraryMisc.ml;h=7c82e27c40f3dd9564674e6d8c7c3c1a2ffb13d8;hb=b44a732a930584aa08f4a78371dd9ac5b405f31e;hp=3f1931e42ce0e979e080c566381f47f572ddbdf8;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/library/libraryMisc.ml b/components/library/libraryMisc.ml
index 3f1931e42..7c82e27c4 100644
--- a/components/library/libraryMisc.ml
+++ b/components/library/libraryMisc.ml
@@ -25,14 +25,14 @@
 
 (* $Id$ *)
 
-let obj_file_of_baseuri ~basedir ~baseuri =
- let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
-  path ^ ".moo"
+let resolve ~must_exist ~writable ~local baseuri = 
+  if must_exist then 
+    Http_getter.resolve ~local ~writable baseuri
+  else 
+    Http_getter.filename ~local ~writable baseuri
 
-let lexicon_file_of_baseuri ~basedir ~baseuri =
- let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
-  path ^ ".lexicon"
+let obj_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable ~local:true baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon"
 
-let metadata_file_of_baseuri ~basedir ~baseuri =
- let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
-  path ^ ".metadata"