src/Pure/RAW/ml_debugger.ML
author wenzelm
Tue Jan 05 13:48:51 2016 +0100 (2016-01-05)
changeset 62058 1cfd5d604937
parent 61925 ab52f183f020
permissions -rw-r--r--
updated headers;
     1 (*  Title:      Pure/RAW/ml_debugger.ML
     2     Author:     Makarius
     3 
     4 ML debugger interface -- dummy version.
     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 * 'location -> unit) option -> unit
    14   val on_exit: (string * 'location -> unit) option -> unit
    15   val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
    16   val on_breakpoint: ('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 -> '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
    33 with
    34 
    35 fun exn_id exn = Exn_Id (General.exnName exn);
    36 fun print_exn_id (Exn_Id name) = name;
    37 fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
    38 
    39 end;
    40 
    41 
    42 (* hooks *)
    43 
    44 fun on_entry _ = ();
    45 fun on_exit _ = ();
    46 fun on_exit_exception _ = ();
    47 fun on_breakpoint _ = ();
    48 
    49 
    50 (* debugger *)
    51 
    52 fun fail () = raise Fail "No debugger support on this ML platform";
    53 
    54 type state = unit;
    55 
    56 fun state _ = [];
    57 fun debug_function () = fail ();
    58 fun debug_function_arg () = fail ();
    59 fun debug_function_result () = fail ();
    60 fun debug_location () = fail ();
    61 fun debug_name_space () = fail ();
    62 fun debug_local_name_space () = fail ();
    63 
    64 end;