Backporting from v8.2 to trunk:

- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 27 insertions, 25 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 867297a86..3246c1478 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -20,14 +20,13 @@ let guess_coqlib () =
     then Coq_config.coqlib
     else 
       let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in
-      let coqlib = if Coq_config.local then prefix else 
+      let coqlib = if !Flags.boot || Coq_config.local then prefix else 
 	List.fold_left Filename.concat prefix ["lib";"coq"] in
 	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
 	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
 	  
 let coqlib () = 
-  if !Flags.coqlib_spec then !Flags.coqlib else
-    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+  if !Flags.coqlib_spec then !Flags.coqlib else guess_coqlib ()
 
 let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
diff --git a/lib/flags.ml b/lib/flags.ml
index c3033c4b5..c0af148c7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -13,6 +13,11 @@ let with_option o f x =
   try let r = f x in o := old; r
   with e -> o := old; raise e
 
+let without_option o f x =
+  let old = !o in o:=false;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
 let boot = ref false
 
 let batch_mode = ref false
@@ -44,16 +49,8 @@ let make_silent flag = silent := flag; ()
 let is_silent () = !silent
 let is_verbose () = not !silent
 
-let silently f x =
-  let oldsilent = !silent in
-  try 
-    silent := true;
-    let rslt = f x in
-    silent := oldsilent; 
-    rslt
-  with e -> begin
-    silent := oldsilent; raise e
-  end
+let silently f x = with_option silent f x
+let verbosely f x = without_option silent f x
 
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
diff --git a/lib/flags.mli b/lib/flags.mli
index f0e4103f6..fe1157d88 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -38,6 +38,7 @@ val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
@@ -46,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option ('c must be an atomic type) *)
+(* Temporary activate an option (to activate option [o] on [f x y z],
+   use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(* Temporary deactivate an option *)
+val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
 (* If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
diff --git a/lib/system.ml b/lib/system.ml
index 00d6dec22..2c63b4cc7 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -128,7 +128,7 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
-let where_in_path warn path filename =
+let where_in_path ?(warn=true) path filename =
   let rec search = function
     | lpe :: rem ->
 	let f = Filename.concat lpe filename in
@@ -144,26 +144,26 @@ let where_in_path warn path filename =
 	    msg_warning
 	      (str filename ++ str " has been found in" ++ spc () ++
 	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep (fun () -> spc() ++ pr_semicolon())
+	         hv 0 (prlist_with_sep (fun () -> str " " ++ 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 =
+let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
     let root = Filename.dirname filename in
     root, filename
   else 
-    try where_in_path true paths filename
+    try where_in_path ~warn 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 false lpath filename); true
+  try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
 let make_suffix name suffix =
@@ -201,7 +201,7 @@ let raw_extern_intern magic suffix =
   in 
   (extern_state,intern_state)
 
-let extern_intern magic suffix =
+let extern_intern ?(warn=true) magic suffix =
   let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
   let extern_state name val_0 = 
     try
@@ -214,7 +214,7 @@ let extern_intern magic suffix =
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name = 
     try
-      let _,filename = find_file_in_path paths (make_suffix name suffix) in
+      let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
       let channel = raw_intern filename in
       let v = marshal_in channel in
       close_in channel; 
diff --git a/lib/system.mli b/lib/system.mli
index 48e02cb5d..7556ed9e4 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -22,7 +22,7 @@ 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 : bool -> load_path -> string -> physical_path * string
+val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
@@ -36,7 +36,8 @@ val home : string
 
 val exists_dir : string -> bool
 
-val find_file_in_path : load_path -> string -> physical_path * string
+val find_file_in_path :
+  ?warn:bool -> load_path -> string -> physical_path * string
 
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
@@ -50,8 +51,8 @@ exception Bad_magic_number of string
 val raw_extern_intern : int -> string -> 
   (string -> string * out_channel) * (string -> in_channel)
 
-val extern_intern : 
-  int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
+val extern_intern : ?warn:bool -> int -> string -> 
+  (string -> 'a -> unit) * (load_path -> string -> 'a)
 
 (*s Sending/receiving once with external executable *)