X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Flexicon%2FlexiconEngine.ml;h=6e3c1b53d2c5aff600c98ea970689c493dc737e1;hb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;hp=aec759c964d64d3b3d00f9ea92d87c73d42a5445;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index aec759c96..6e3c1b53d 100644
--- a/components/lexicon/lexiconEngine.ml
+++ b/components/lexicon/lexiconEngine.ml
@@ -36,6 +36,14 @@ type status = {
   metadata: LibraryNoDb.metadata list;
 }
 
+let initial_status = {
+  aliases = DisambiguateTypes.Environment.empty;
+  multi_aliases = DisambiguateTypes.Environment.empty;
+  lexicon_content_rev = [];
+  notation_ids = [];
+  metadata = [];
+}
+
 let add_lexicon_content cmds status =
   let content = status.lexicon_content_rev in
   let content' =
@@ -100,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) ->