src/Pure/ML/exn_debugger.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62821 48c24d0b6d85
child 62891 7a11ea5c9626
permissions -rw-r--r--
clarified modules;
tuned signature;
     1 (*  Title:      Pure/ML/exn_debugger.ML
     2     Author:     Makarius
     3 
     4 Detailed exception trace via ML debugger.
     5 *)
     6 
     7 signature EXN_DEBUGGER =
     8 sig
     9   val capture_exception_trace:
    10     (unit -> 'a) -> (string * ML_Compiler0.polyml_location) list * 'a Exn.result
    11 end;
    12 
    13 structure Exn_Debugger: EXN_DEBUGGER =
    14 struct
    15 
    16 (* thread data *)
    17 
    18 val trace_var =
    19   Thread_Data.var () : ((string * ML_Compiler0.polyml_location) * exn) list Thread_Data.var;
    20 
    21 fun start_trace () = Thread_Data.put trace_var (SOME []);
    22 
    23 fun 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 
    28 fun 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 
    34 val _ = ML_Debugger.on_exit_exception (SOME update_trace);
    35 
    36 
    37 (* capture exception trace *)
    38 
    39 local
    40   fun eq_exn exns =
    41     op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Properties.position exns);
    42 in
    43 
    44 fun capture_exception_trace e =
    45   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 
    59 end;
    60 
    61 end;