added default for matita.noiinertypes

[helm.git] / components / library / libraryMisc.ml

diff --git a/components/library/libraryMisc.ml b/components/library/libraryMisc.ml
index 148b5f8bc905b077691a6c06c61100b648e8db36..7c82e27c40f3dd9564674e6d8c7c3c1a2ffb13d8 100644 (file)
--- a/components/library/libraryMisc.ml
+++ b/components/library/libraryMisc.ml
@@ -25,12 +25,14 @@
 
 (* $Id$ *)
 
-let resolve ~writable baseuri = Http_getter.filename ~writable baseuri
+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 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 ~local:true baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon"