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