X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibraryMisc.ml;h=e971c52d4b09cfe489ac27facb5e0c43729de748;hb=e53dfd3fa17a77ab1fdd249ed2e5b6d0f9d94d88;hp=148b5f8bc905b077691a6c06c61100b648e8db36;hpb=ee3f8d6fa92b051394a2ff7c71c03ac33a05182b;p=helm.git

diff --git a/helm/software/components/library/libraryMisc.ml b/helm/software/components/library/libraryMisc.ml
index 148b5f8bc..e971c52d4 100644
--- a/helm/software/components/library/libraryMisc.ml
+++ b/helm/software/components/library/libraryMisc.ml
@@ -25,12 +25,16 @@
 
 (* $Id$ *)
 
-let resolve ~writable baseuri = Http_getter.filename ~writable baseuri
+let resolve ~must_exist ~writable baseuri = 
+  if must_exist then 
+    Http_getter.resolve ~writable baseuri
+  else 
+    Http_getter.filename ~writable baseuri
 
-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 obj_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".lexicon"
+let metadata_file_of_baseuri~must_exist ~writable  ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".metadata"