--- a/src/Pure/RAW/ml_debugger.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML Thu Mar 03 11:12:02 2016 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/RAW/ml_debugger.ML
Author: Makarius
-ML debugger interface -- dummy version.
+ML debugger interface -- for Poly/ML 5.6, or later.
*)
signature ML_DEBUGGER =
@@ -10,16 +10,17 @@
val exn_id: exn -> exn_id
val print_exn_id: exn_id -> string
val eq_exn_id: exn_id * exn_id -> bool
- 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 location
+ 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_location: state -> location
val debug_name_space: state -> ML_Name_Space.T
val debug_local_name_space: state -> ML_Name_Space.T
end;
@@ -29,36 +30,43 @@
(* exceptions *)
-abstype exn_id = Exn_Id of string
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
with
-fun exn_id exn = Exn_Id (General.exnName exn);
-fun print_exn_id (Exn_Id name) = name;
-fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2; (*over-approximation*)
+fun exn_id exn =
+ Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
end;
+val _ =
+ PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+ let val s = print_exn_id exn_id
+ in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+
(* hooks *)
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-(* debugger *)
+(* debugger operations *)
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
+type state = PolyML.DebuggerInterface.debugState;
-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 ();
-fun debug_local_name_space () = fail ();
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
end;