diff options
| -rw-r--r-- | tools/coqdep.ml | 6 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 22 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 6 |
3 files changed, 22 insertions, 12 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 08c42b7eb..f90620b2f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -495,9 +495,9 @@ let coqdep () = (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath; end; - List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; - List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu; + List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; + List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; + List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; warning_mult ".mli" iter_mli_known; warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d7532dba6..25fd49082 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -103,9 +103,17 @@ let safe_hash_add clq q (k,v) = For the ML files, the string is the basename without extension. *) +let warning_ml_clash x s s' suff = + eprintf + "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + (match s with None -> "." | Some d -> d) + ((match s' with None -> "." | Some d -> d) // x) suff + let mkknown () = let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in - let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s + let add x s suff = + try let s' = Hashtbl.find h x in warning_ml_clash x s' s suff + with Not_found -> Hashtbl.add h x s and iter f = Hashtbl.iter f h and search x = try Some (Hashtbl.find h x) @@ -428,11 +436,13 @@ let rec suffixes = function | dir::suffix as l -> l::suffixes suffix let add_caml_known phys_dir _ f = - match get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] with - | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) - | (basename,".mli") -> add_mli_known basename (Some phys_dir) - | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) - | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir) + let basename,suff = + get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + match suff with + | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".mli" -> add_mli_known basename (Some phys_dir) suff + | ".mllib" -> add_mllib_known basename (Some phys_dir) suff + | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () let add_known recur phys_dir log_dir f = diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 3c1cd4fbe..9a10be317 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -23,13 +23,13 @@ val mliAccu : (string * dir) list ref val mllibAccu : (string * dir) list ref val vAccu : (string * string) list ref val addQueue : 'a list ref -> 'a -> unit -val add_ml_known : string -> dir -> unit +val add_ml_known : string -> dir -> string -> unit val iter_ml_known : (string -> dir -> unit) -> unit val search_ml_known : string -> dir option -val add_mli_known : string -> dir -> unit +val add_mli_known : string -> dir -> string -> unit val iter_mli_known : (string -> dir -> unit) -> unit val search_mli_known : string -> dir option -val add_mllib_known : string -> dir -> unit +val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option val vKnown : (string list, string) Hashtbl.t val coqlibKnown : (string list, unit) Hashtbl.t |