Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

5 files changed, 83 insertions, 42 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index de971c7c..16ae0c64 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.ml 11077 2008-06-09 11:26:32Z herbelin $ i*)
-
-open Util
+(*i $Id: flags.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -78,6 +76,8 @@ let print_hyps_limit () = !print_hyps_limit
 (* A list of the areas of the system where "unsafe" operation
  * has been requested *)
 
+module Stringset = Set.Make(struct type t = string let compare = compare end)
+
 let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
@@ -126,7 +126,4 @@ let browser_cmd_fmt =
   let coq_netscape_remote_var = "COQREMOTEBROWSER" in
   Sys.getenv coq_netscape_remote_var
  with
-  Not_found ->
-   if Sys.os_type = "Win32"
-   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"
-   else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
+  Not_found -> Coq_config.browser
diff --git a/lib/system.ml b/lib/system.ml
index aa71ddfa..22eb52ee 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 10437 2008-01-11 14:50:44Z bertot $ *)
+(* $Id: system.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
 
 open Pp
 open Util
@@ -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 6d535464..eb83cbf8 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli 9398 2006-11-21 21:51:18Z herbelin $ i*)
+(*i $Id: system.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
@@ -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
diff --git a/lib/util.ml b/lib/util.ml
index 9fa92f94..75ee4246 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11083 2008-06-09 22:08:14Z herbelin $ *)
+(* $Id: util.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 
@@ -576,6 +576,12 @@ let list_fold_left_i f =
   in 
   it_list_f 
 
+let rec list_fold_left3 f accu l1 l2 l3 =
+  match (l1, l2, l3) with
+    ([], [], []) -> accu
+  | (a1::l1, a2::l2, a3::l3) -> list_fold_left3 f (f accu a1 a2 a3) l1 l2 l3
+  | (_, _, _) -> invalid_arg "list_fold_left3"
+
 (* [list_fold_right_and_left f [a1;...;an] hd =
    f (f (... (f (f hd
                    an
@@ -1196,6 +1202,8 @@ let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
 let nth n = str (ordinal n)
 
+(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
+
 let rec prlist elem l = match l with 
   | []   -> mt ()
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
@@ -1207,6 +1215,9 @@ let rec prlist_strict elem l = match l with
   | []   -> mt ()
   | h::t -> (elem h)++(prlist_strict elem t)
 
+(* [prlist_with_sep sep pr [a ; ... ; c]] outputs
+   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
+
 let rec prlist_with_sep sep elem l = match l with
   | []   -> mt ()
   | [h]  -> elem h
@@ -1214,6 +1225,23 @@ let rec prlist_with_sep sep elem l = match l with
       let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
       e ++ s ++ r
 
+(* Print sequence of objects separated by space (unless an element is empty) *)
+
+let rec pr_sequence elem = function
+  | []   -> mt ()
+  | [h]  -> elem h
+  | h::t ->
+      let e = elem h and r = pr_sequence elem t in
+      if e = mt () then r else e ++ spc () ++ r
+
+(* [pr_enum pr [a ; b ; ... ; c]] outputs 
+   [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *)
+
+let pr_enum pr l =
+  let c,l' = list_sep_last l in
+  prlist_with_sep pr_coma pr l' ++
+  (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c
+
 let pr_vertical_list pr = function
   | [] -> str "none" ++ fnl ()
   | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
@@ -1228,6 +1256,9 @@ let prvecti elem v =
   in
   if n = 0 then mt () else pr (n - 1)
 
+(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs
+   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
+
 let prvect_with_sep sep elem v =
   let rec pr n =
     if n = 0 then 
@@ -1239,8 +1270,16 @@ let prvect_with_sep sep elem v =
   let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *)
+
 let prvect elem v = prvect_with_sep mt elem v
 
+let pr_located pr (loc,x) =
+  if Flags.do_translate() && loc<>dummy_loc then
+    let (b,e) = unloc loc in
+    comment b ++ pr x ++ comment e
+  else pr x
+
 let surround p = hov 1 (str"(" ++ p ++ str")")
 
 (*s Size of ocaml values. *)
diff --git a/lib/util.mli b/lib/util.mli
index 7807bbbd..99ad3c03 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11083 2008-06-09 22:08:14Z herbelin $ i*)
+(*i $Id: util.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -132,6 +132,7 @@ val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
     ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
+val list_fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_remove : 'a -> 'a list -> 'a list
@@ -279,6 +280,9 @@ val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prvect_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
+val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds