diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 50 |
1 files changed, 24 insertions, 26 deletions
diff --git a/library/library.ml b/library/library.ml index 56d2709d..0ff82d7c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -167,7 +167,7 @@ let opened_libraries () = !libraries_imports_list let register_loaded_library m = let libname = m.libsum_name in - let link m = + let link () = let dirname = Filename.dirname (library_full_filename libname) in let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in @@ -176,7 +176,7 @@ let register_loaded_library m = Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link m; [libname] + | [] -> link (); [libname] | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; @@ -288,16 +288,15 @@ let locate_absolute_library dir = try let name = Id.to_string base ^ ext in let _, file = System.where_in_path ~warn:false loadpath name in - [file] - with Not_found -> [] in - match find ".vo" @ find ".vio" with - | [] -> raise LibNotFound - | [file] -> file - | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + Some file + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some file, None | None, Some file -> file + | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> warn_several_object_files (vi, vo); vi - | [vo;vi] -> vo - | _ -> assert false + | Some vo, Some _ -> vo let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) @@ -309,18 +308,17 @@ let locate_qualified_library ?root ?(warn = true) qid = let name = Id.to_string base ^ ext in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - [lpath, file] - with Not_found -> [] in + Some (lpath, file) + with Not_found -> None in let lpath, file = - match find ".vo" @ find ".vio" with - | [] -> raise LibNotFound - | [lpath, file] -> lpath, file - | [lpath_vo, vo; lpath_vi, vi] + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some res, None | None, Some res -> res + | Some (_, vo), Some (_, vi as resvi) when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> warn_several_object_files (vi, vo); - lpath_vi, vi - | [lpath_vo, vo; _ ] -> lpath_vo, vo - | _ -> assert false + resvi + | Some resvo, Some _ -> resvo in let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in (* Look if loaded *) @@ -577,10 +575,10 @@ let require_library_from_dirpath modrefl export = (* the function called by Vernacentries.vernac_import *) -let safe_locate_module {CAst.loc;v=qid} = +let safe_locate_module qid = try Nametab.locate_module qid with Not_found -> - user_err ?loc ~hdr:"import_library" + user_err ?loc:qid.CAst.loc ~hdr:"import_library" (pr_qualid qid ++ str " is not a module") let import_module export modl = @@ -595,18 +593,18 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | ({CAst.loc; v=dir} as m) :: l -> + | qid :: l -> let m,acc = - try Nametab.locate_module dir, acc - with Not_found-> flush acc; safe_locate_module m, [] in + try Nametab.locate_module qid, acc + with Not_found-> flush acc; safe_locate_module qid, [] in (match m with | MPfile dir -> aux (dir::acc) l | mp -> flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err ?loc ~hdr:"import_library" - (pr_qualid dir ++ str " is not a module")) + user_err ?loc:qid.CAst.loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module")) | [] -> flush acc in aux [] modl |