Restrict (try...with...) to avoid catching critical exn (part 15)

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

3 files changed, 29 insertions, 19 deletions

diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index f848591cc9..6fd79f16b2 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -148,7 +148,7 @@ let real_nonlinear_prover d l =
    S (Some proof)
  with
   | Sos_lib.TooDeep -> S None
-  |    x        ->   F (Printexc.to_string x)
+  | any -> F (Printexc.to_string any)
 
 (* This is somewhat buggy, over Z, strict inequality vanish... *)
 let pure_sos  l =
@@ -172,7 +172,7 @@ let pure_sos  l =
     S (Some proof)
  with
 (*   | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
-   |  x        -> (* May be that could be refined *) S None
+   | any -> (* May be that could be refined *) S None
 
 
 
@@ -201,7 +201,7 @@ let main () =
       Marshal.to_channel  chan (cert:csdp_certificate) [] ;
       flush chan ;
       exit 0
-  with  x -> (Printf.fprintf chan "error %s" (Printexc.to_string x)  ; exit 1)
+  with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any)  ; exit 1)
 
 ;;
 
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 43cad05e94..0b98696c95 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -29,10 +29,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any -> raise reraise
+    ); raise reraise
 
 let map_option f x =
   match x with
@@ -429,16 +429,26 @@ let command exe_path args vl =
 	(fun () ->
 	  match status with
 	    | Unix.WEXITED 0 ->
-		let inch  = Unix.in_channel_of_descr stdout_read in
-		  begin try Marshal.from_channel inch 
-                        with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) 
-                  end
-	    | Unix.WEXITED i   -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
-	    | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
-	    | Unix.WSTOPPED i  -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
+		let inch = Unix.in_channel_of_descr stdout_read in
+		begin
+                  try Marshal.from_channel inch
+                  with any ->
+                    failwith
+                      (Printf.sprintf "command \"%s\" exited %s" exe_path
+                         (Printexc.to_string any))
+                end
+	    | Unix.WEXITED i   ->
+                failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
+	    | Unix.WSIGNALED i ->
+                failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
+	    | Unix.WSTOPPED i  ->
+                failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
         (* Cleanup  *)
 	(fun () ->
-	  List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
+	  List.iter (fun x -> try Unix.close x with any -> ())
+            [stdin_read; stdin_write;
+             stdout_read; stdout_write;
+             stderr_read; stderr_write])
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cb7a9280d4..39a1b82b0d 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -82,10 +82,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any -> raise reraise
+    ); raise reraise
 
 
 let read_key_elem inch =
@@ -93,7 +93,7 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    |    _        -> raise InvalidTableFormat
+    | e when Errors.noncritical e -> raise InvalidTableFormat
 
 (** In win32, it seems that we should unlock the exact zone
     that has been locked, and not the whole file *)
@@ -151,7 +151,7 @@ let open_in f =
 	    Table.iter 
 	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
 	    flush outch ; 
-	  with  _ -> () )
+	  with e when Errors.noncritical e -> () )
 	    ;
 	    unlock out ; 
 	    { outch = outch ;