]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/libraryMisc.ml
Huge commit for the release. Includes:
[helm.git] / components / library / libraryMisc.ml
index 3f1931e42ce0e979e080c566381f47f572ddbdf8..148b5f8bc905b077691a6c06c61100b648e8db36 100644 (file)
 
 (* $Id$ *)
 
-let obj_file_of_baseuri ~basedir ~baseuri =
- let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
-  path ^ ".moo"
+let resolve ~writable baseuri = Http_getter.filename ~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 ~writable ~baseuri = 
+  resolve ~writable baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~writable ~baseuri = 
+  resolve ~writable baseuri ^ ".lexicon"
+let metadata_file_of_baseuri~writable  ~baseuri = 
+  resolve ~writable baseuri ^ ".metadata"
 
-let metadata_file_of_baseuri ~basedir ~baseuri =
- let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
-  path ^ ".metadata"