Actually adding backtrace handling.

I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.

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

7 files changed, 45 insertions, 22 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b4d0bc4134..525a924ed9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -13,6 +13,7 @@ let (/) = Filename.concat
 
 let set_debug () =
   let () = Printexc.record_backtrace true in
+  let () = Errors.record_backtrace () in
   Flags.debug := true
 
 (* Loading of the ressource file.
@@ -51,8 +52,9 @@ let load_rcfile() =
 			 " found. Skipping rcfile loading."))
 	*)
     with e ->
-      (msg_info (str"Load of rcfile failed.");
-       raise e)
+      let e = Errors.push e in
+      let () = msg_info (str"Load of rcfile failed.") in
+      raise e
   else
     Flags.if_verbose msg_info (str"Skipping rcfile loading.")
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a785dd31a4..1e41cdec8f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -267,6 +267,7 @@ let parse_format ((loc, str) : lstring) =
     else
       error "Empty format."
   with e ->
+    let e = Errors.push e in
     Loc.raise loc e
 
 (***********************)
@@ -1072,7 +1073,10 @@ let inNotation : notation_obj -> obj =
 let with_lib_stk_protection f x =
   let fs = Lib.freeze () in
   try let a = f x in Lib.unfreeze fs; a
-  with e -> Lib.unfreeze fs; raise e
+  with e ->
+    let e = Errors.push e in
+    let () = Lib.unfreeze fs in
+    raise e
 
 let with_syntax_protection f x =
   with_lib_stk_protection
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 4ac6adc354..59059a77af 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -117,12 +117,15 @@ let dir_ml_load s =
     | WithTop t ->
       (try t.load_obj s
        with
-       | (UserError _ | Failure _ | Not_found as u) -> raise u
-       | u when Errors.is_anomaly u -> raise u
-       | exc ->
-           let msg = report_on_load_obj_error exc in
-           errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
-                str s ++ str" to Coq code (" ++ msg ++ str ")."))
+       | e ->
+        let e = Errors.push e in
+        match e with
+        | (UserError _ | Failure _ | Not_found as u) -> raise u
+        | u when is_anomaly u -> reraise u
+        | exc ->
+            let msg = report_on_load_obj_error exc in
+            errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+                  str s ++ str" to Coq code (" ++ msg ++ str ")."))
     | WithoutTop ->
         let warn = Flags.is_verbose() in
         let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 68dfca9f93..6ec01f5474 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -736,6 +736,7 @@ let solve_by_tac evi t =
 	const.Entries.const_entry_body;
       const.Entries.const_entry_body
   with e ->
+    let e = Errors.push e in
     Pfedit.delete_current_proof();
     raise e
 
@@ -818,13 +819,15 @@ and solve_obligation_by_tac prg obls i tac =
 	      obls.(i) <- declare_obligation prg obl t;
 	      true
 	  else false
-	with
-	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Loc.Exc_located(_, Refiner.FailError (_, s))
-	| Refiner.FailError (_, s) ->
-	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-	| e when Errors.is_anomaly e -> raise e
-	| e -> false
+	with e ->
+          let e = Errors.push e in
+          match e with
+          | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+          | Loc.Exc_located(_, Refiner.FailError (_, s))
+          | Refiner.FailError (_, s) ->
+              user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+          | e when is_anomaly e -> raise e
+          | e -> false
 
 and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7a17a2b31e..cb8962a9b9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -284,6 +284,7 @@ let rec vernac_com interpfun checknav (loc,com) =
 	    restore_translator_coqdoc st;
             status
 	  with e ->
+            let e = Errors.push e in
 	    restore_translator_coqdoc st;
 	    raise e
 	end
@@ -298,7 +299,9 @@ let rec vernac_com interpfun checknav (loc,com) =
 	  (* If the command actually works, ignore its effects on the state *)
 	  States.with_state_protection
 	    (fun v -> ignore (interp v); raise HasNotFailed) v
-	with e -> match real_error e with
+	with e ->
+          let e = Errors.push e in
+          match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")
 	  | e ->
@@ -331,7 +334,10 @@ let rec vernac_com interpfun checknav (loc,com) =
             in
 	    restore_timeout psh;
             status
-	  with e -> restore_timeout psh; raise e
+	  with e ->
+            let e = Errors.push e in
+            restore_timeout psh;
+            raise e
   in
     try
       checknav loc com;
@@ -341,6 +347,7 @@ let rec vernac_com interpfun checknav (loc,com) =
       let com = if !time then VernacTime com else com in
       interp com
     with e ->
+      let e = Errors.push e in
       Format.set_formatter_out_channel stdout;
       raise (DuringCommandInterp (loc, e))
 
@@ -375,6 +382,7 @@ and read_vernac_file verbosely s =
     done;
     assert false
   with e ->   (* whatever the exception *)
+    let e = Errors.push e in
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
@@ -420,6 +428,7 @@ let load_vernac verb file =
     let _ = read_vernac_file verb file in
     if !Flags.beautify_file then close_out !chan_beautify;
   with e ->
+    let e = Errors.push e in
     if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file e
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7e681b1a08..8fb3aa66b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1791,11 +1791,12 @@ let interp c =
     interp c; Locality.check_locality ();
     Flags.program_mode := mode;
     true
-  with
+  with e ->
+    let e = Errors.push e in
+    match e with
     | UnsafeSuccess ->
         Flags.program_mode := mode;
         false
     | e ->
-    Flags.program_mode := mode;
-    raise e
-
+      Flags.program_mode := mode;
+      raise e
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index dca47f7146..fdfa514278 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -55,6 +55,7 @@ let call (opn,converted_args) =
   with
     | Drop -> raise Drop
     | e ->
+        let e = Errors.push e in
         if !Flags.debug then
 	  msg_debug (str"Vernac Interpreter " ++ str !loc);
         raise e