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
+ ~must_exist:false ~writable:true ~baseuri,
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~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
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~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) ->