diff options
Diffstat (limited to 'toplevel/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 41 |
1 files changed, 16 insertions, 25 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 59bc01d0..ff3ce8a0 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,18 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_macro.cmo" i*) -(* WARNING - * camlp4deps will not work for this file unless Makefile system enhanced. - *) - -(* $Id: mltop.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Pp open Flags @@ -133,8 +126,8 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path *) -let add_rec_ml_dir dir = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs dir) +let add_rec_ml_dir unix_path = + List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) (* Adding files to Coq and ML loadpath *) @@ -150,24 +143,24 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d with _ -> - if_verbose warning - ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + if_warn msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); failwith "caught" -let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - if exists_dir dir then - let dirs = all_subdirs dir in - let prefix = Names.repr_dirpath coq_dirpath in +let add_rec_path ~unix_path ~coq_root = + if exists_dir unix_path then + let dirs = all_subdirs ~unix_path in + let prefix = Names.repr_dirpath coq_root in let convert_dirs (lp,cp) = (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - add_ml_dir dir; + add_ml_dir unix_path; List.iter (Library.add_load_path false) dirs; - Library.add_load_path true (dir,coq_dirpath) + Library.add_load_path true (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str ("Cannot open " ^ unix_path)) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -224,8 +217,6 @@ let file_of_name name = coqtop could always load plugins, we prefer to have uniformity between bytecode and native versions. *) -let stdlib_use_plugins = Coq_config.has_natdynlink - (* [known_loaded_module] contains the names of the loaded ML modules * (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. *) @@ -244,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 @@ -266,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."); @@ -291,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 -> @@ -305,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = let classify_ml_module_object ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o -let (inMLModule,outMLModule) = +let inMLModule : ml_module_object -> obj = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; |