src/Pure/ML-Systems/ml_debugger.ML

resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;

(*  Title:      Pure/ML/ml_debugger.ML
    Author:     Makarius

ML debugger interface -- dummy version.
*)

signature ML_DEBUGGER =
sig
  val on_entry: (string * 'location -> unit) option -> unit
  val on_exit: (string * 'location -> unit) option -> unit
  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
  type state
  val state: Thread.thread -> state list
  val debug_function: state -> string
  val debug_function_arg: state -> ML_Name_Space.valueVal
  val debug_function_result: state -> ML_Name_Space.valueVal
  val debug_location: state -> 'location
  val debug_name_space: state -> ML_Name_Space.T
end;

structure ML_Debugger: ML_DEBUGGER =
struct

(* hooks *)

fun on_entry _ = ();
fun on_exit _ = ();
fun on_exit_exception _ = ();
fun on_breakpoint _ = ();


(* debugger *)

fun fail () = raise Fail "No debugger support on this ML platform";

type state = unit;

fun state _ = [];
fun debug_function () = fail ();
fun debug_function_arg () = fail ();
fun debug_function_result () = fail ();
fun debug_location () = fail ();
fun debug_name_space () = fail ();

end;