diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 59 | ||||
| -rw-r--r-- | lib/system.mli | 4 |
2 files changed, 32 insertions, 31 deletions
diff --git a/lib/system.ml b/lib/system.ml index c5ed94d5c..4f21c8746 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -68,6 +68,14 @@ let string_of_physical_path p = p let exists_dir dir = try let _ = opendir dir in true with Unix_error _ -> false +let skipped_dirnames = ref ["CVS"; "_darcs"] + +let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames + +let ok_dirname f = + f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && + try ignore (check_ident f); true with _ -> false + let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in @@ -76,8 +84,7 @@ let all_subdirs ~unix_path:root = try while true do let f = readdir dirh in - if f <> "" && f.[0] <> '.' && (not Coq_config.local or (f <> "CVS")) - then + if ok_dirname f then let file = Filename.concat dir f in try if (stat file).st_kind = S_DIR then begin @@ -90,52 +97,44 @@ let all_subdirs ~unix_path:root = with End_of_file -> closedir dirh in - if exists_dir root then - begin - add root []; - traverse root [] - end ; + if exists_dir root then traverse root []; List.rev !l -let where_in_path path filename = - let rec search acc = function +let where_in_path warn path filename = + let rec search = function | lpe :: rem -> let f = Filename.concat lpe filename in if Sys.file_exists f - then (search ((lpe,f)::acc) rem) - else search acc rem - | [] -> acc in - let rec check_and_warn cont acc l = + then (lpe,f) :: search rem + else search rem + | [] -> [] in + let rec check_and_warn l = match l with - | [] -> if cont then assert false else raise Not_found - | [ (lpe, f) ] -> - if cont then begin - warning (acc ^ (string_of_physical_path lpe) ^ " ]"); - warning ("Loading " ^ f) - end; - (lpe, f) + | [] -> raise Not_found | (lpe, f) :: l' -> - if cont then - check_and_warn true (acc ^ (string_of_physical_path lpe) ^ "; ") l' - else - check_and_warn true - (filename ^ " has been found in [ " ^ (string_of_physical_path lpe) ^ "; ") l' - in - check_and_warn false "" (search [] path) - + if warn & l' <> [] then + msg_warning + (str filename ++ str " has been found in" ++ spc () ++ + hov 0 (str "[ " ++ + hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l) + ++ str " ];") ++ fnl () ++ + str "loading " ++ str f); + (lpe, f) in + check_and_warn (search path) + let find_file_in_path paths filename = if not (Filename.is_implicit filename) then let root = Filename.dirname filename in root, filename else - try where_in_path paths filename + try where_in_path true paths filename with Not_found -> errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) let is_in_path lpath filename = - try ignore (where_in_path lpath filename); true + try ignore (where_in_path false lpath filename); true with Not_found -> false let make_suffix name suffix = diff --git a/lib/system.mli b/lib/system.mli index 1292ec77d..6c607607f 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -16,9 +16,11 @@ type physical_path = string type load_path = physical_path list +val exclude_search_in_dirname : string -> unit + val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool -val where_in_path : load_path -> string -> physical_path * string +val where_in_path : bool -> load_path -> string -> physical_path * string val physical_path_of_string : string -> physical_path val string_of_physical_path : physical_path -> string |