From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Sep 2015 12:25:35 +0200 Subject: The -require option now accepts a logical path instead of a physical one. --- library/library.ml | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index 1bcffcd14..a09f91b15 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,18 +488,8 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let check_library_short_name f dir = function - | Some id when not (Id.equal id (snd (split_dirpath dir))) -> - errorlabstrm "check_library_short_name" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ - pr_id id) - | _ -> () - -let rec_intern_by_filename_only id f = +let rec_intern_by_filename_only f = let m = try intern_from_file f with Sys_error s -> error s in - (* Only the base name is expected to match *) - check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin @@ -518,12 +508,12 @@ let native_name_from_filename f = let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file idopt f = +let rec_intern_library_from_file f = (* A name is specified, we have to check it contains library id *) let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only idopt f + rec_intern_by_filename_only f (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a @@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file idopt file export = - let modref,needed = rec_intern_library_from_file idopt file in +let require_library_from_file file export = + let modref,needed = rec_intern_library_from_file file in let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); -- cgit v1.2.3