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