1(*  Title:      Pure/ML/exn_debugger.ML
2    Author:     Makarius
3
4Detailed exception trace via ML debugger.
5*)
6
7signature EXN_DEBUGGER =
8sig
9  val capture_exception_trace:
10    (unit -> 'a) -> (string * ML_Compiler0.polyml_location) list * 'a Exn.result
11end;
12
13structure Exn_Debugger: EXN_DEBUGGER =
14struct
15
16(* thread data *)
17
18val trace_var =
19  Thread_Data.var () : ((string * ML_Compiler0.polyml_location) * exn) list Thread_Data.var;
20
21fun start_trace () = Thread_Data.put trace_var (SOME []);
22
23fun update_trace entry exn =
24  (case Thread_Data.get trace_var of
25    SOME trace => Thread_Data.put trace_var (SOME ((entry, exn) :: trace))
26  | NONE => ());
27
28fun stop_trace () =
29  let
30    val trace = the_default [] (Thread_Data.get trace_var);
31    val _ = Thread_Data.put trace_var NONE;
32  in trace end;
33
34val _ = PolyML.DebuggerInterface.setOnExitException (SOME update_trace);
35
36
37(* capture exception trace *)
38
39local
40  fun eq_exn exns =
41    op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Properties.position exns);
42in
43
44fun capture_exception_trace e =
45  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
46    let
47      val _ = start_trace ();
48      val result = Exn.interruptible_capture (restore_attributes e) ();
49      val trace = stop_trace ();
50      val trace' =
51        (case result of
52          Exn.Res _ => []
53        | Exn.Exn exn =>
54            trace
55            |> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
56            |> rev);
57    in (trace', result) end) ();
58
59end;
60
61end;
62