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

6 files changed, 63 insertions, 16 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 342ec10225..e1a8d46b76 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -8,26 +8,35 @@
 
 open Pp
 
-(* Errors *)
+(** Aliases *)
+
+let push = Backtrace.push_exn
 
-type backtrace = string option
+let reraise = Backtrace.reraise
 
-exception Anomaly of string option * std_ppcmds * backtrace (* System errors *)
+(* Errors *)
 
-let get_backtrace () =
-  if !Flags.debug then Some (Printexc.get_backtrace ())
-  else None
+exception Anomaly of string option * std_ppcmds * Backtrace.t (* System errors *)
 
 let make_anomaly ?label pp =
-  let bt = get_backtrace () in
+  let bt =
+    if !Flags.debug then Backtrace.empty
+    else Backtrace.none
+  in
   Anomaly (label, pp, bt)
 
 let anomaly_gen label pp =
-  let bt = get_backtrace () in
+  let bt =
+    if !Flags.debug then Backtrace.empty
+    else Backtrace.none
+  in
   raise (Anomaly (label, pp, bt))
 
 let anomaly ?loc ?label pp =
-  let bt = get_backtrace () in
+  let bt =
+    if !Flags.debug then Backtrace.empty
+    else Backtrace.none
+  in
   match loc with
   | None -> raise (Anomaly (label, pp, bt))
   | Some loc ->
@@ -96,7 +105,10 @@ let raw_anomaly e = match e with
 
 let print_anomaly askreport e =
   let bt_info = match e with
-  | Anomaly (_, _, Some bt) -> (fnl () ++ hov 0 (str bt))
+  | Anomaly (_, _, Some bt) ->
+    let pr_frame f = str (Backtrace.print_frame f) in
+    let bt = prlist_with_sep fnl pr_frame bt in
+    fnl () ++ hov 0 bt
   | _ -> mt ()
   in
   let info =
@@ -127,3 +139,21 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
+let rec anomaly_handler = function
+| Anomaly (lbl, pp, bt) ->
+  let bt = Backtrace.push bt in
+  Some (Anomaly (lbl, pp, bt))
+| Loc.Exc_located (loc, e) ->
+  begin match anomaly_handler e with
+  | None -> None
+  | Some e -> Some (Loc.Exc_located (loc, e))
+  end
+| Error_in_file (s, data, e) ->
+  begin match anomaly_handler e with
+  | None -> None
+  | Some e -> Some (Error_in_file (s, data, e))
+  end
+| e -> None
+
+let record_backtrace () =
+  Backtrace.register_backtrace_handler anomaly_handler
diff --git a/lib/errors.mli b/lib/errors.mli
index 00c39c2b3d..d596abb55a 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -11,6 +11,14 @@ open Pp
 (** This modules implements basic manipulations of errors for use
     throughout Coq's code. *)
 
+(** {6 Error handling} *)
+
+val push : exn -> exn
+(** Alias for [Backtrace.push_exn]. *)
+
+val reraise : exn -> 'a
+(** Alias for [Backtrace.reraise]. *)
+
 (** {6 Generic errors.}
 
  [Anomaly] is used for system errors and [UserError] for the
@@ -85,3 +93,6 @@ 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
+
+(** Enable registering of backtrace information. *)
+val record_backtrace : unit -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index 765574cb4b..b4c72b38a1 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 e -> o := old; Backtrace.reraise e
 
 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 e -> o := old; Backtrace.reraise e
 
 let boot = ref false
 
diff --git a/lib/pp.ml b/lib/pp.ml
index b899ef8231..b9dc05edff 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -262,8 +262,10 @@ let pp_dirs ft =
   fun (dirstream : _ ppdirs) ->
     try
       Stream.iter pp_dir dirstream; com_brk ft
-    with
-      | e -> Format.pp_print_flush ft () ; raise e
+    with e ->
+      let e = Backtrace.push_exn e in
+      let () = Format.pp_print_flush ft () in
+      raise e
 
 
 (* pretty print on stdout and stderr *)
diff --git a/lib/system.ml b/lib/system.ml
index dbab923af0..ed23bde197 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -142,7 +142,9 @@ let extern_intern ?(warn=true) magic suffix =
         marshal_out channel val_0;
         close_out channel
       with e ->
-	begin try_remove filename; raise e end
+	let e = Errors.push e in
+        let () = try_remove filename in
+        raise e
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 81fefd8805..108e226783 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -166,7 +166,9 @@ let error_of_exn xparser = function
   | NoMoreData -> NodeExpected
   | Internal_error e -> e
   | Xml_lexer.Error e -> convert e
-  | e -> raise e
+  | e ->
+    (*let e = Errors.push e in: We do not record backtrace here. *)
+    raise e
 
 let do_parse xparser =
 	try