diff options
| -rw-r--r-- | toplevel/mltop.ml | 78 |
1 files changed, 52 insertions, 26 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 7f421c2644..c609a6e241 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -112,10 +112,11 @@ let report_on_load_obj_error exc = else str (Printexc.to_string exc) (* Dynamic loading of .cmo/.cma *) -let dir_ml_load s = + +let ml_load s = match !load with | WithTop t -> - (try t.load_obj s + (try t.load_obj s; s with | e when Errors.noncritical e -> let e = Errors.push e in @@ -126,15 +127,21 @@ let dir_ml_load s = errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ str s ++ str" to Coq code (" ++ msg ++ str ").")) | WithoutTop -> - let warn = Flags.is_verbose() in - let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in try - Dynlink.loadfile gname; + Dynlink.loadfile s; s with Dynlink.Error a -> errorlabstrm "Mltop.load_object" (strbrk "while loading " ++ str s ++ strbrk ": " ++ str (Dynlink.error_message a)) +let dir_ml_load s = + match !load with + | WithTop _ -> ml_load s + | WithoutTop -> + let warn = Flags.is_verbose() in + let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in + ml_load gname + (* Dynamic interpretation of .ml *) let dir_ml_use s = match !load with @@ -215,7 +222,9 @@ let file_of_name name = errorlabstrm "Mltop.load_object" (str"File not found on loadpath : " ++ str s ++ str"\n" ++ str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in - if is_native then + if not (Filename.is_relative name) then + if Sys.file_exists name then name else fail name + else if is_native then let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> (Filename.chop_suffix name suffix) ^ ".cmxs" @@ -248,20 +257,25 @@ let file_of_name name = * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) -let known_loaded_modules = ref String.Set.empty +let known_loaded_modules = ref String.Map.empty -let add_known_module mname = - known_loaded_modules := String.Set.add mname !known_loaded_modules +let add_known_module mname path = + if not (String.Map.mem mname !known_loaded_modules) || + String.Map.find mname !known_loaded_modules = None then + known_loaded_modules := String.Map.add mname path !known_loaded_modules let module_is_known mname = - String.Set.mem mname !known_loaded_modules + String.Map.mem mname !known_loaded_modules + +let known_module_path mname = + String.Map.find mname !known_loaded_modules (** A plugin is just an ML module with an initialization function. *) let known_loaded_plugins = ref String.Map.empty let add_known_plugin init name = - add_known_module name; + add_known_module name None; known_loaded_plugins := String.Map.add name init !known_loaded_plugins let init_known_plugins () = @@ -288,11 +302,16 @@ let init_ml_object mname = try String.Map.find mname !known_loaded_plugins () with Not_found -> () -let load_ml_object mname fname= - dir_ml_load fname; - add_known_module mname; - init_ml_object mname +let load_ml_object mname ?path fname= + let path = match path with + | None -> dir_ml_load fname + | Some p -> ml_load p in + add_known_module mname (Some path); + init_ml_object mname; + path +let dir_ml_load m = ignore(dir_ml_load m) +let add_known_module m = add_known_module m None let load_ml_object_raw fname = dir_ml_load (file_of_name fname) let load_ml_objects_raw_rex rex = List.iter (fun (_,fp) -> dir_ml_load (file_of_name (Filename.basename fp))) @@ -304,16 +323,19 @@ let load_ml_objects_raw_rex rex = let loaded_modules = ref [] let get_loaded_modules () = List.rev !loaded_modules -let add_loaded_module md = loaded_modules := md :: !loaded_modules +let add_loaded_module md path = + if not (List.mem_assoc md !loaded_modules) then + loaded_modules := (md,path) :: !loaded_modules let reset_loaded_modules () = loaded_modules := [] -let if_verbose_load verb f name fname = - if not verb then f name fname +let if_verbose_load verb f name ?path fname = + if not verb then f name ?path fname else let info = "[Loading ML file "^fname^" ..." in try - f name fname; + let path = f name ?path fname in msg_info (str (info^" done]")); + path with reraise -> msg_info (str (info^" failed]")); raise reraise @@ -322,23 +344,27 @@ let if_verbose_load verb f name fname = or simulate its reload (i.e. doing nothing except maybe an initialization function). *) -let trigger_ml_object verb cache reinit name = +let trigger_ml_object verb cache reinit ?path name = if module_is_known name then begin if reinit then init_ml_object name; - add_loaded_module name; + add_loaded_module name (known_module_path name); if cache then perform_cache_obj name end else if not has_dynlink then error ("Dynamic link not supported (module "^name^")") else begin - let file = file_of_name name in - if_verbose_load (verb && is_verbose ()) load_ml_object name file; - add_loaded_module name; + let file = file_of_name (Option.default name path) in + let path = + if_verbose_load (verb && is_verbose ()) load_ml_object name ?path file in + add_loaded_module name (Some path); if cache then perform_cache_obj name end +let load_ml_object n m = ignore(load_ml_object n m) + let unfreeze_ml_modules x = reset_loaded_modules (); - List.iter (trigger_ml_object false false false) x + List.iter + (fun (name,path) -> trigger_ml_object false false false ?path name) x let _ = Summary.declare_summary Summary.ml_modules @@ -385,7 +411,7 @@ let print_ml_path () = let print_ml_modules () = let l = get_loaded_modules () in - str"Loaded ML Modules: " ++ pr_vertical_list str l + str"Loaded ML Modules: " ++ pr_vertical_list str (List.map fst l) let print_gc () = let stat = Gc.stat () in |