src/Pure/ML/exn_debugger.ML
changeset 62889 99c7f31615c2
parent 62821 48c24d0b6d85
child 62891 7a11ea5c9626
     1.1 --- a/src/Pure/ML/exn_debugger.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/ML/exn_debugger.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -15,28 +15,24 @@
     1.4  
     1.5  (* thread data *)
     1.6  
     1.7 -local
     1.8 -  val tag =
     1.9 -    Universal.tag () : ((string * ML_Compiler0.polyml_location) * exn) list option Universal.tag;
    1.10 -in
    1.11 +val trace_var =
    1.12 +  Thread_Data.var () : ((string * ML_Compiler0.polyml_location) * exn) list Thread_Data.var;
    1.13  
    1.14 -fun start_trace () = Thread.setLocal (tag, SOME []);
    1.15 +fun start_trace () = Thread_Data.put trace_var (SOME []);
    1.16  
    1.17  fun update_trace entry exn =
    1.18 -  (case Thread.getLocal tag of
    1.19 -    SOME (SOME trace) => Thread.setLocal (tag, SOME ((entry, exn) :: trace))
    1.20 -  | _ => ());
    1.21 +  (case Thread_Data.get trace_var of
    1.22 +    SOME trace => Thread_Data.put trace_var (SOME ((entry, exn) :: trace))
    1.23 +  | NONE => ());
    1.24  
    1.25  fun stop_trace () =
    1.26    let
    1.27 -    val trace = (case Thread.getLocal tag of SOME (SOME trace) => trace | _ => []);
    1.28 -    val _ = Thread.setLocal (tag, NONE);
    1.29 +    val trace = the_default [] (Thread_Data.get trace_var);
    1.30 +    val _ = Thread_Data.put trace_var NONE;
    1.31    in trace end;
    1.32  
    1.33  val _ = ML_Debugger.on_exit_exception (SOME update_trace);
    1.34  
    1.35 -end;
    1.36 -
    1.37  
    1.38  (* capture exception trace *)
    1.39