Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

7 files changed, 78 insertions, 14 deletions

diff --git a/lib/options.ml b/lib/options.ml
index 0d934922..2e29f61b 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: options.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
+(* $Id: options.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Util
 
@@ -70,11 +70,11 @@ let print_hyps_limit () = !print_hyps_limit
 
 (* A list of the areas of the system where "unsafe" operation
  * has been requested *)
+
 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
 
-
 (* Dump of globalization (to be used by coqdoc) *)
 
 let dump = ref false
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index e7ba9869..88efc5f2 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,10 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp.ml4 7751 2005-12-28 12:58:53Z herbelin $ *)
+(* $Id: pp.ml4 8747 2006-04-27 16:00:49Z courtieu $ *)
 
 open Pp_control
 
+(* This should not be used outside of this file. Use
+   Options.print_emacs instead. This one is updated when reading
+   command line options. This was the only way to make [Pp] depend on
+   an option without creating a circularity: [Options] -> [Util] ->
+   [Pp] -> [Options] *)
+let print_emacs = ref false
+let make_pp_emacs() = print_emacs:=true
+
 (* The different kinds of blocks are: 
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -238,6 +246,17 @@ let pp_err_dirs = pp_dirs err_ft
 
 let ppcmds x = Ppdir_ppcmds x
 
+(* Special chars for emacs, to detect warnings inside goal output *)
+let emacs_warning_start_string = String.make 1 (Char.chr 254)
+let emacs_warning_end_string = String.make 1 (Char.chr 255)
+
+let warnstart() = 
+  if not !print_emacs then str "" else str emacs_warning_start_string
+
+let warnend() = 
+  if not !print_emacs then str "" else str emacs_warning_end_string
+  
+
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds strm >]
@@ -246,10 +265,10 @@ let ppnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
 
 let warning_with ft string =
-  ppnl_with ft [< str "Warning: " ; str string >]
+  ppnl_with ft [< warnstart() ; str "Warning: " ; str string ; warnend() >]
 
 let warn_with ft pps =
-  ppnl_with ft [< str "Warning: " ; pps >]
+  ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >]
 
 let pp_flush_with ft =
   Format.pp_print_flush ft
@@ -263,7 +282,7 @@ let msgnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
 
 let msg_warning_with ft strm=
-  pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; 
+  pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >]; 
 		'Ppdir_print_newline >]
 
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 88deb6d2..e240fd2d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,12 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: pp.mli 8748 2006-04-27 16:01:26Z courtieu $ i*)
 
 (*i*)
 open Pp_control
 (*i*)
 
+(* Modify pretty printing functions behavior for emacs ouput (special
+   chars inserted at some places). This function should called once in
+   module [Options], that's all. *)
+val make_pp_emacs:unit -> unit
+
 (* Pretty-printers. *)
 
 type ppcmd
diff --git a/lib/system.ml b/lib/system.ml
index fb3cf7b5..b8be9956 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 7603 2005-11-23 17:21:53Z barras $ *)
+(* $Id: system.ml 8877 2006-05-30 16:37:04Z notin $ *)
 
 open Pp
 open Util
@@ -60,6 +60,9 @@ let glob s = expand_macros s 0
 type physical_path = string
 type load_path = physical_path list
 
+let physical_path_of_string s = s
+let string_of_physical_path p = p
+
 (* All subdirectories, recursively *)
 
 let exists_dir dir =
diff --git a/lib/system.mli b/lib/system.mli
index ea463732..2fea77ed 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 7603 2005-11-23 17:21:53Z barras $ i*)
+(*i $Id: system.mli 8877 2006-05-30 16:37:04Z notin $ 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
@@ -20,6 +20,9 @@ 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 physical_path_of_string : string -> physical_path
+val string_of_physical_path : physical_path -> string
+
 val make_suffix : string -> string -> string
 val file_readable_p : string -> bool
 
diff --git a/lib/util.ml b/lib/util.ml
index 2e6e1279..503dfeda 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
+(* $Id: util.ml 8867 2006-05-28 16:21:41Z herbelin $ *)
 
 open Pp
 
@@ -214,6 +214,16 @@ let list_index x =
   in 
   index_x 1
 
+let list_unique_index x = 
+  let rec index_x n = function
+    | y::l -> 
+	if x = y then 
+	  if List.mem x l then raise Not_found
+	  else n 
+	else index_x (succ n) l
+    | [] -> raise Not_found 
+  in index_x 1
+
 let list_fold_left_i f = 
   let rec it_list_f i a = function
     | [] -> a 
@@ -353,7 +363,19 @@ let list_prefix_of prefl l =
     | ([], _) -> true
     | (_, _) -> false
   in 
-  prefrec (prefl,l)
+    prefrec (prefl,l)
+
+let list_drop_prefix p l =
+(* if l=p++t then return t else l *)
+  let rec list_drop_prefix_rec = function
+    | ([], tl) -> Some tl
+    | (_, []) -> None
+    | (h1::tp, h2::tl) -> 
+	if h1 = h2 then list_drop_prefix_rec (tp,tl) else None
+  in
+    match list_drop_prefix_rec (p,l) with
+      | Some r -> r
+      | None -> l
 
 let list_map_append f l = List.flatten (List.map f l)
 
@@ -620,6 +642,13 @@ else
   let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
   (v',!e')
 
+let array_fold_map2' f v1 v2 e =
+  let e' = ref e in
+  let v' = 
+    array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 
+  in
+  (v',!e')
+
 (* Matrices *)
 
 let matrix_transpose mat =
@@ -672,7 +701,7 @@ let out_some = function
   | Some x -> x
   | None -> failwith "out_some"
 
-let option_app f = function
+let option_map f = function
   | None -> None
   | Some x -> Some (f x)
 
diff --git a/lib/util.mli b/lib/util.mli
index f77aa6b4..959ef802 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 8672 2006-03-29 21:06:33Z herbelin $ i*)
+(*i $Id: util.mli 8867 2006-05-28 16:21:41Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -100,6 +100,8 @@ val list_map2_i :
 val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
 val list_index : 'a -> 'a list -> int
+(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+val list_unique_index : 'a -> 'a list -> int 
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
@@ -121,6 +123,7 @@ val list_last : 'a list -> 'a
 val list_lastn : int -> 'a list -> 'a list
 val list_skipn : int -> 'a list -> 'a list 
 val list_prefix_of : 'a list -> 'a list -> bool
+val list_drop_prefix : 'a list -> 'a list -> 'a list
 (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 (* raises [Invalid_argument] if the two lists don't have the same length *)
@@ -170,6 +173,8 @@ val array_map_left : ('a -> 'b) -> 'a array -> 'b array
 val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
   'b array * 'd array
 val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+val array_fold_map2' :
+  ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 
 (*s Matrices *)
 
@@ -199,7 +204,7 @@ val interval : int -> int -> int list
 
 val in_some : 'a -> 'a option
 val out_some : 'a option -> 'a
-val option_app : ('a -> 'b) -> 'a option -> 'b option
+val option_map : ('a -> 'b) -> 'a option -> 'b option
 val option_cons : 'a option -> 'a list -> 'a list
 val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->