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