Huge commit for the release. Includes:

[helm.git] / components / lexicon / lexiconEngine.ml

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index 4adfe624b2039c4042e925a6ed2641e1c0b37c98..6e3c1b53d2c5aff600c98ea970689c493dc737e1 100644 (file)
--- a/components/lexicon/lexiconEngine.ml
+++ b/components/lexicon/lexiconEngine.ml
@@ -108,20 +108,30 @@ let rec eval_command status cmd =
  let notation_ids' = CicNotation.process_notation cmd in
  let status =
    { status with notation_ids = notation_ids' @ status.notation_ids } in
- let basedir = Helm_registry.get "matita.basedir" in
   match cmd with
   | LexiconAst.Include (loc, baseuri) ->
-     let lexiconpath = LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in
-     if not (Sys.file_exists lexiconpath) then
-       raise (IncludedFileNotCompiled lexiconpath);
+     let lexiconpath_rw, lexiconpath_r = 
+       LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri,
+       LibraryMisc.lexicon_file_of_baseuri ~writable:false ~baseuri
+     in
+     let lexiconpath = 
+       if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
+         if Sys.file_exists lexiconpath_r then lexiconpath_r else
+          raise (IncludedFileNotCompiled lexiconpath_rw)
+     in
      let lexicon = LexiconMarshal.load_lexicon lexiconpath in
      let status = List.fold_left eval_command status lexicon in
       if Helm_registry.get_bool "db.nodb" then
-       let metadatapath = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
-        if not (Sys.file_exists metadatapath) then
-          raise (MetadataNotFound metadatapath)
-        else
-          add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
+       let metadatapath_rw, metadatapath_r = 
+         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true,
+         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:false
+       in
+       let metadatapath =
+        if Sys.file_exists metadatapath_rw then metadatapath_rw else
+         if Sys.file_exists metadatapath_r then metadatapath_r else
+           raise (MetadataNotFound metadatapath_rw)
+       in
+         add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
       else
          status
   | LexiconAst.Alias (loc, spec) ->