Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

11 files changed, 70 insertions, 42 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 4ec68a27..c672d30c 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -23,6 +23,8 @@ let _ =
   if Coq_config.arch = "win32" then
     Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
 
+let exe s = s ^ Coq_config.exec_extension
+
 let reldir instdir testfile oth =
   let rpath = if Coq_config.local then [] else instdir in
   let out = List.fold_left Filename.concat coqroot rpath in
@@ -87,19 +89,19 @@ let rec which l f =
 	else which tl f
 
 let guess_camlbin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath "ocamlc"
+    which lpath (exe "ocamlc")
 
 let guess_camlp4bin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath Coq_config.camlp4
+    which lpath (exe Coq_config.camlp4)
 
 let camlbin () =
   if !Flags.camlbin_spec then !Flags.camlbin else
     if !Flags.boot then Coq_config.camlbin else
-      try guess_camlbin () with _ -> Coq_config.camlbin
+      try guess_camlbin () with e when e <> Sys.Break -> Coq_config.camlbin
 
 let camllib () =
   if !Flags.boot
@@ -113,9 +115,10 @@ let camllib () =
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
     if !Flags.boot then Coq_config.camlp4bin else
-      try guess_camlp4bin () with _ -> let cb = camlbin () in
-				       if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb
-				       else Coq_config.camlp4bin
+      try guess_camlp4bin () with e when e <> Sys.Break ->
+        let cb = camlbin () in
+	if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb
+	else Coq_config.camlp4bin
 
 let camlp4lib () =
   if !Flags.boot
diff --git a/lib/errors.ml b/lib/errors.ml
index 3b5e6770..6affea23 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -28,7 +28,7 @@ let rec print_gen bottom stk e =
     try h e
     with
     | Unhandled -> print_gen bottom stk' e
-    | e' -> print_gen bottom stk' e'
+    | any -> print_gen bottom stk' any
 
 (** Only anomalies should reach the bottom of the handler stack.
     In usual situation, the [handle_stack] is treated as it if was always
@@ -66,3 +66,14 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only at the very end of interp, to be displayed to the user. *)
+
+(** NB: in the 8.4 branch, for maximal compatibility, anomalies
+    are considered non-critical *)
+
+let noncritical = function
+  | Sys.Break | Out_of_memory | Stack_overflow -> false
+  | _ -> true
+
diff --git a/lib/errors.mli b/lib/errors.mli
index eb7fde8e..ae4d0b85 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -39,3 +39,11 @@ val print_no_report : exn -> Pp.std_ppcmds
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
+    Typical example: [Sys.Break]. In the 8.4 branch, for maximal
+    compatibility, anomalies are not considered as critical...
+*)
+val noncritical : exn -> bool
diff --git a/lib/flags.ml b/lib/flags.ml
index 3474573e..32c68b25 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,12 +9,12 @@
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
-  with e -> o := old; raise e
+  with reraise -> o := old; raise reraise
 
 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
+  with reraise -> o := old; raise reraise
 
 let boot = ref false
 
diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml
index 2780afe8..bb2252da 100644
--- a/lib/hashtbl_alt.ml
+++ b/lib/hashtbl_alt.ml
@@ -89,7 +89,7 @@ module Make (E : Hashtype) =
 		match rest2 with
 		  | Empty -> add hash key; key
 		  | Cons (k3, h3, rest3) ->
-		    if hash == h2 && E.equals key k3 then k3
+		    if hash == h3 && E.equals key k3 then k3
 		    else find_rec hash key rest3
 
 end
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 7777d091..569a028f 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -279,7 +279,7 @@ let pp_dirs ft =
     try
       Stream.iter pp_dir dirstream; com_brk ft
     with
-      | e -> Format.pp_print_flush ft () ; raise e
+      | reraise -> Format.pp_print_flush ft () ; raise reraise
 
 
 (* pretty print on stdout and stderr *)
diff --git a/lib/profile.ml b/lib/profile.ml
index 2472d75d..39e08721 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
       let _dw = dummy_spent_alloc () in
       let _dt = get_time () in
       ()
-    with _ -> assert false
+    with e when e <> Sys.Break -> assert false
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
@@ -390,7 +390,7 @@ let profile1 e f a =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -403,7 +403,7 @@ let profile1 e f a =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile2 e f a b =
   let dw = spent_alloc () in
@@ -432,7 +432,7 @@ let profile2 e f a b =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -445,7 +445,7 @@ let profile2 e f a b =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile3 e f a b c =
   let dw = spent_alloc () in
@@ -474,7 +474,7 @@ let profile3 e f a b c =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -487,7 +487,7 @@ let profile3 e f a b c =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile4 e f a b c d =
   let dw = spent_alloc () in
@@ -516,7 +516,7 @@ let profile4 e f a b c d =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -529,7 +529,7 @@ let profile4 e f a b c d =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile5 e f a b c d g =
   let dw = spent_alloc () in
@@ -558,7 +558,7 @@ let profile5 e f a b c d g =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -571,7 +571,7 @@ let profile5 e f a b c d g =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile6 e f a b c d g h =
   let dw = spent_alloc () in
@@ -600,7 +600,7 @@ let profile6 e f a b c d g h =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -613,7 +613,7 @@ let profile6 e f a b c d g h =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile7 e f a b c d g h i =
   let dw = spent_alloc () in
@@ -642,7 +642,7 @@ let profile7 e f a b c d g h i =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -655,7 +655,7 @@ let profile7 e f a b c d g h i =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 (* Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
diff --git a/lib/store.ml b/lib/store.ml
index bc1b335f..28eb65c8 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -53,7 +53,7 @@ let field () =
   in
   let get s =
     try Some (Obj.obj (Util.Intmap.find fid s))
-    with _ -> None
+    with Not_found -> None
   in
   let remove s =
     Util.Intmap.remove fid s
diff --git a/lib/system.ml b/lib/system.ml
index a99c29f2..ae637708 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -140,7 +140,8 @@ 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
+  try ignore (check_ident f); true
+  with e when e <> Sys.Break -> false
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
@@ -223,17 +224,22 @@ let file_readable_p name =
   try access name [R_OK];true with Unix_error (_, _, _) -> false
 
 let open_trapping_failure name =
-  try open_out_bin name with _ -> error ("Can't open " ^ name)
+  try open_out_bin name
+  with e when e <> Sys.Break -> error ("Can't open " ^ name)
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str filename ++ str" which is corrupted!" )
+  with e when e <> Sys.Break ->
+    msgnl (str"Warning: " ++ str"Could not remove file " ++
+             str filename ++ str" which is corrupted!" )
 
 let marshal_out ch v = Marshal.to_channel ch v []
-let marshal_in ch =
+let marshal_in filename ch =
   try Marshal.from_channel ch
-  with End_of_file -> error "corrupted file: reached end of file"
+  with
+    | End_of_file -> error "corrupted file: reached end of file"
+    | Failure _ (* e.g. "truncated object" *) ->
+        error (filename ^ " is corrupted, try to rebuild it.")
 
 exception Bad_magic_number of string
 
@@ -259,14 +265,14 @@ let extern_intern ?(warn=true) magic suffix =
       try
         marshal_out channel val_0;
         close_out channel
-      with e ->
-	begin try_remove filename; raise e end
+      with reraise ->
+	begin try_remove filename; raise reraise end
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
       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
+      let v = marshal_in filename channel in
       close_in channel;
       v
     with Sys_error s ->
diff --git a/lib/system.mli b/lib/system.mli
index 4a79b874..d8420e7d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -47,7 +47,7 @@ val find_file_in_path :
   when the check fails, with the full file name. *)
 
 val marshal_out : out_channel -> 'a -> unit
-val marshal_in : in_channel -> 'a
+val marshal_in : string -> in_channel -> 'a
 
 exception Bad_magic_number of string
 
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 19bab4f6..600796f7 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -175,7 +175,7 @@ let do_parse xparser source =
 		if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
 		Xml_lexer.close source;
 		x
-	with e ->
+	with e when e <> Sys.Break ->
 	  Xml_lexer.close source;
 	  raise (!xml_error (error_of_exn stk e) source)
 
@@ -190,9 +190,9 @@ let parse p = function
 			close_in ch;
 			x
 		with
-			e ->
+			reraise ->
 				close_in ch;
-				raise e
+				raise reraise
 
 
 let error_msg = function