src/Pure/ML/ml_debugger.ML
author wenzelm
Sat Apr 02 22:13:00 2016 +0200 (2016-04-02 ago)
changeset 62822 941b6a48ff67
parent 62821 48c24d0b6d85
child 62934 6e3fb0aa857a
permissions -rw-r--r--
tuned;
wenzelm@62508
     1
(*  Title:      Pure/ML/ml_debugger.ML
wenzelm@60732
     2
    Author:     Makarius
wenzelm@60732
     3
wenzelm@61794
     4
ML debugger interface -- for Poly/ML 5.6, or later.
wenzelm@60732
     5
*)
wenzelm@60732
     6
wenzelm@60852
     7
signature ML_DEBUGGER =
wenzelm@60852
     8
sig
wenzelm@60954
     9
  type exn_id
wenzelm@60954
    10
  val exn_id: exn -> exn_id
wenzelm@60954
    11
  val print_exn_id: exn_id -> string
wenzelm@60954
    12
  val eq_exn_id: exn_id * exn_id -> bool
wenzelm@62821
    13
  val on_entry: (string * ML_Compiler0.polyml_location -> unit) option -> unit
wenzelm@62821
    14
  val on_exit: (string * ML_Compiler0.polyml_location -> unit) option -> unit
wenzelm@62821
    15
  val on_exit_exception: (string * ML_Compiler0.polyml_location -> exn -> unit) option -> unit
wenzelm@62821
    16
  val on_breakpoint: (ML_Compiler0.polyml_location * bool Unsynchronized.ref -> unit) option -> unit
wenzelm@60852
    17
  type state
wenzelm@60852
    18
  val state: Thread.thread -> state list
wenzelm@60852
    19
  val debug_function: state -> string
wenzelm@60852
    20
  val debug_function_arg: state -> ML_Name_Space.valueVal
wenzelm@60852
    21
  val debug_function_result: state -> ML_Name_Space.valueVal
wenzelm@62821
    22
  val debug_location: state -> ML_Compiler0.polyml_location
wenzelm@60852
    23
  val debug_name_space: state -> ML_Name_Space.T
wenzelm@61888
    24
  val debug_local_name_space: state -> ML_Name_Space.T
wenzelm@60852
    25
end;
wenzelm@60852
    26
wenzelm@60732
    27
structure ML_Debugger: ML_DEBUGGER =
wenzelm@60732
    28
struct
wenzelm@60732
    29
wenzelm@60954
    30
(* exceptions *)
wenzelm@60954
    31
wenzelm@60954
    32
abstype exn_id = Exn_Id of string * int Unsynchronized.ref
wenzelm@60954
    33
with
wenzelm@60954
    34
wenzelm@60954
    35
fun exn_id exn =
wenzelm@60954
    36
  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
wenzelm@60954
    37
wenzelm@60954
    38
fun print_exn_id (Exn_Id (name, _)) = name;
wenzelm@62822
    39
fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = pointer_eq (id1, id2);
wenzelm@60954
    40
wenzelm@60954
    41
end;
wenzelm@60954
    42
wenzelm@60954
    43
val _ =
wenzelm@62819
    44
  ML_system_pp (fn _ => fn _ => fn exn_id =>
wenzelm@60954
    45
    let val s = print_exn_id exn_id
wenzelm@62503
    46
    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
wenzelm@60954
    47
wenzelm@60954
    48
wenzelm@60732
    49
(* hooks *)
wenzelm@60732
    50
wenzelm@60732
    51
val on_entry = PolyML.DebuggerInterface.setOnEntry;
wenzelm@60732
    52
val on_exit = PolyML.DebuggerInterface.setOnExit;
wenzelm@60732
    53
val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
wenzelm@60744
    54
val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
wenzelm@60732
    55
wenzelm@60732
    56
wenzelm@60732
    57
(* debugger operations *)
wenzelm@60732
    58
wenzelm@60732
    59
type state = PolyML.DebuggerInterface.debugState;
wenzelm@60732
    60
wenzelm@60732
    61
val state = PolyML.DebuggerInterface.debugState;
wenzelm@60732
    62
val debug_function = PolyML.DebuggerInterface.debugFunction;
wenzelm@60732
    63
val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
wenzelm@60732
    64
val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
wenzelm@60732
    65
val debug_location = PolyML.DebuggerInterface.debugLocation;
wenzelm@60732
    66
val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
wenzelm@61888
    67
val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
wenzelm@60732
    68
wenzelm@60732
    69
end;