1 files changed, 81 insertions, 66 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 9bdcecef..4b99de70 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,38 +9,32 @@
 (* $Id$ *)
 
 open Pp
-open Errors
 open Util
 
-(* All subdirectories, recursively *)
+include Minisys
 
-let exists_dir dir =
-  try Sys.is_directory dir with Sys_error _ -> false
+(** Returns the list of all recursive subdirectories of [root] in
+    depth-first search, with sons ordered as on the file system;
+    warns if [root] does not exist *)
 
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
-  not (String.is_empty f) && f.[0] != '.' &&
-  not (String.List.mem f !skipped_dirnames) &&
-  (match Unicode.ident_refutation f with None -> true | _ -> false)
+let warn_cannot_open_dir =
+  CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
+  (fun dir -> str ("Cannot open directory " ^ dir))
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
-  let rec traverse dir rel =
-    Array.iter (fun f ->
-      if ok_dirname f then
-	let file = Filename.concat dir f in
-        if Sys.is_directory file then begin
-          let newrel = rel @ [f] in
-	  add file newrel;
-	  traverse file newrel
-        end)
-      (Sys.readdir dir)
+  let rec traverse path rel =
+    let f = function
+      | FileDir (path,f) ->
+	  let newrel = rel @ [f] in
+	  add path newrel;
+	  traverse path newrel
+      | _ -> ()
+    in process_directory f path
   in
-  if exists_dir root then traverse root [];
+  if exists_dir root then traverse root []
+  else warn_cannot_open_dir root;
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -58,23 +52,25 @@ let dirmap = ref StrMap.empty
 
 let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
-  Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+  Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
 
 let exists_in_dir_respecting_case dir bf =
-  let contents, cached =
-    try StrMap.find dir !dirmap, true with Not_found ->
+  let cache_dir dir =
     let contents = make_dir_table dir in
     dirmap := StrMap.add dir contents !dirmap;
-    contents, false in
+    contents in
+  let contents, fresh =
+    try
+      (* in batch mode, assume the directory content is still fresh *)
+      StrMap.find dir !dirmap, !Flags.batch_mode
+    with Not_found ->
+      (* in batch mode, we are not yet sure the directory exists *)
+      if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+      else cache_dir dir, true in
   StrSet.mem bf contents ||
-    if cached then begin
+    not fresh &&
       (* rescan, there is a new file we don't know about *)
-      let contents = make_dir_table dir in
-      dirmap := StrMap.add dir contents !dirmap;
-      StrSet.mem bf contents
-    end
-    else
-      false
+      StrSet.mem bf (cache_dir dir)
 
 let file_exists_respecting_case path f =
   (* This function ensures that a file with expected lowercase/uppercase
@@ -84,26 +80,29 @@ let file_exists_respecting_case path f =
     let df = Filename.dirname f in
     (String.equal df "." || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
-  in Sys.file_exists (Filename.concat path f) && aux f
+  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
   | [] -> []
   | lpe :: rem -> test lpe @ search rem test
 
+let warn_ambiguous_file_name =
+  CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
+    (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
+                hov 0 (str "[ " ++
+                         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+                                               (fun (lpe,_) -> str lpe) l)
+                       ++ str " ];") ++ fnl () ++
+                str "loading " ++ str f)
+
+
 let where_in_path ?(warn=true) path filename =
   let check_and_warn l = match l with
   | [] -> raise Not_found
   | (lpe, f) :: l' ->
     let () = match l' with
-    | _ :: _ when warn ->
-      msg_warning
-        (str filename ++ str " has been found in" ++ spc () ++
-          hov 0 (str "[ " ++
-            hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
-              (fun (lpe,_) -> str lpe) l)
-            ++ str " ];") ++ fnl () ++
-          str "loading " ++ str f)
+    | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
     | _ -> ()
     in
     (lpe, f)
@@ -132,7 +131,7 @@ let find_file_in_path ?(warn=true) paths filename =
       let root = Filename.dirname filename in
       root, filename
     else
-      errorlabstrm "System.find_file_in_path"
+      CErrors.errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
     (* the name is considered to be the transcription as a relative
@@ -140,7 +139,7 @@ let find_file_in_path ?(warn=true) paths filename =
        to be locate respecting case *)
     try where_in_path ~warn paths filename
     with Not_found ->
-      errorlabstrm "System.find_file_in_path"
+      CErrors.errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
 		str "on loadpath"))
 
@@ -148,25 +147,34 @@ let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
+let warn_path_not_found =
+  CWarnings.create ~name:"path-not-found" ~category:"filesystem"
+  (fun () -> str "system variable PATH not found")
+
 let is_in_system_path filename =
-  let path = try Sys.getenv "PATH"
-             with Not_found -> error "system variable PATH not found" in
-  let lpath = CUnix.path_to_list path in
-  is_in_path lpath filename
+  try
+    let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
+    is_in_path lpath filename
+  with Not_found ->
+    warn_path_not_found ();
+    false
 
 let open_trapping_failure name =
   try open_out_bin name
-  with e when Errors.noncritical e ->
-    errorlabstrm "System.open" (str "Can't open " ++ str name)
+  with e when CErrors.noncritical e ->
+    CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name)
+
+let warn_cannot_remove_file =
+  CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
+  (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let try_remove filename =
   try Sys.remove filename
-  with e when Errors.noncritical e ->
-    msg_warning
-      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+  with e when CErrors.noncritical e ->
+    warn_cannot_remove_file filename
 
 let error_corrupted file s =
-  errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+  CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -210,7 +218,8 @@ let skip_in_segment f ch =
   seek_in ch stop;
   stop, digest_in f ch
 
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
 
 let raw_extern_state magic filename =
   let channel = open_trapping_failure filename in
@@ -220,8 +229,12 @@ let raw_extern_state magic filename =
 let raw_intern_state magic filename =
   try
     let channel = open_in_bin filename in
-    if not (Int.equal (input_binary_int filename channel) magic) then
-      raise (Bad_magic_number filename);
+    let actual_magic = input_binary_int filename channel in
+    if not (Int.equal actual_magic magic) then
+        raise (Bad_magic_number {
+            filename=filename;
+            actual=actual_magic;
+            expected=magic});
     channel
   with
   | End_of_file -> error_corrupted filename "premature end of file"
@@ -234,11 +247,11 @@ let extern_state magic filename val_0 =
       marshal_out channel val_0;
       close_out channel
     with reraise ->
-      let reraise = Errors.push reraise in
+      let reraise = CErrors.push reraise in
       let () = try_remove filename in
       iraise reraise
   with Sys_error s ->
-    errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+    CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s)
 
 let intern_state magic filename =
   try
@@ -247,13 +260,15 @@ let intern_state magic filename =
     close_in channel;
     v
   with Sys_error s ->
-    errorlabstrm "System.intern_state" (str "System error: " ++ str s)
+    CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
-  with Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+  with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
+    CErrors.errorlabstrm "with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+    int actual ++ str" (expected " ++ int expected ++ str")." ++
+    spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
 (* Time stamps. *)
@@ -284,13 +299,13 @@ let with_time time f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if time then "" else " (successful)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if time then "" else "Finished failing transaction in " in
     let msg2 = if time then "" else " (failure)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 let process_id () =