diff options
| author | herbelin | 2010-10-31 21:19:15 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-31 21:19:15 +0000 |
| commit | f35a2ddd119ca99e924c68e3346a07087811c261 (patch) | |
| tree | d44b62f7c09f284ba05a48191866a80359d4f6c0 | |
| parent | 5b7992d4650e0aea9c34cdc08c00d292a000928c (diff) | |
Minor code improvements around libobject
- renamed load_object in mltop into load_ml_object to avoid confusion
with load_object in library
- flushed the liboject warning in real time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/libobject.ml | 5 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 6 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 2 |
3 files changed, 7 insertions, 6 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index d9ffe1cd5c..4cc2fdb350 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -143,8 +143,9 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.warning ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)"); + Pp.msg_warning + (Pp.str ("Cannot find library functions for an object with tag " + ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () end; deflt diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 446efc9540..d9a261ed46 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -235,7 +235,7 @@ let add_known_module mname = let module_is_known mname = Stringset.mem (String.capitalize mname) !known_loaded_modules -let load_object mname fname= +let load_ml_object mname fname= dir_ml_load fname; add_known_module mname @@ -257,7 +257,7 @@ let unfreeze_ml_modules x = if not (module_is_known mname) then if has_dynlink then let fname = file_of_name mname in - load_object mname fname + load_ml_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" (str"Loading of ML object file forbidden in a native Coq."); @@ -282,7 +282,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = try if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); - load_object mname fname; + load_ml_object mname fname; if_verbose msgnl (str" done]"); add_loaded_module mname with e -> diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index c625854eae..1e9c3b03c7 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -49,7 +49,7 @@ val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool -val load_object : string -> string -> unit +val load_ml_object : string -> string -> unit (** Summary of Declared ML Modules *) val get_loaded_modules : unit -> string list |