From 9cdf9c3c0341a395249946d9e8f0bed7dd3c6d53 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 24 Dec 2008 14:38:55 +0000 Subject: - coq_makefile: target install now respects the original tree structure of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/coqtop.ml | 16 +++++++++------- toplevel/mltop.ml4 | 12 +++++++----- toplevel/vernacentries.ml | 7 +++++-- toplevel/vernacexpr.ml | 2 +- 4 files changed, 22 insertions(+), 15 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index fec6b0740..9ada5bff2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -51,7 +51,9 @@ let set_batch_mode () = batch_mode := true let toplevel_default_name = make_dirpath [id_of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) -let set_toplevel_name dir = toplevel_name := Some dir +let set_toplevel_name dir = + if dir = empty_dirpath then error "Need a non empty toplevel module name"; + toplevel_name := Some dir let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () @@ -68,16 +70,16 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if !outputstate <> "" then extern_state !outputstate -let check_coq_overwriting p = - if string_of_id (list_last (repr_dirpath p)) = "Coq" then - error "The \"Coq\" logical root directory is reserved for the Coq library" - let set_default_include d = push_include (d,Nameops.default_root_prefix) let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix) let set_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_include (d,p) let set_rec_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index dcdc46e8e..685eaba3f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -47,8 +47,10 @@ open Vernacinterp (* This path is where we look for .cmo *) let coq_mlpath_copy = ref ["."] -let keep_copy_mlpath path = - coq_mlpath_copy := path :: !coq_mlpath_copy +let keep_copy_mlpath path = + let cpath = canonical_path_name path in + let filter path' = (cpath <> canonical_path_name path') in + coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { @@ -106,7 +108,7 @@ let dir_ml_load s = * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. *) - let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in + let _,gname = where_in_path true !coq_mlpath_copy s in try Dynlink.loadfile gname; with | Dynlink.Error a -> @@ -310,10 +312,10 @@ let cache_ml_module_object (_,{mnames=mnames}) = if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl (str"done]"); + if_verbose msgnl (str" done]"); add_loaded_module mname with e -> - if_verbose msgnl (str"failed]"); + if_verbose msgnl (str" failed]"); raise e else if_verbose diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f5603535b..42a06308c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -182,8 +182,11 @@ let show_match id = let print_path_entry (s,l) = (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s) -let print_loadpath () = +let print_loadpath dir = let l = Library.get_full_load_paths () in + let l = match dir with + | None -> l + | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in msgnl (Pp.t (str "Logical Path: " ++ tab () ++ str "Physical path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) @@ -1063,7 +1066,7 @@ let vernac_print = function | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) | PrintGrammar ent -> Metasyntax.print_grammar ent - | PrintLoadPath -> (* For compatibility ? *) print_loadpath () + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8e797a883..d8084c966 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -38,7 +38,7 @@ type printable = | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string - | PrintLoadPath + | PrintLoadPath of dir_path option | PrintModules | PrintModule of reference | PrintModuleType of reference -- cgit v1.2.3