|
1 (* Title: Pure/RAW/ml_debugger_polyml-5.6.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 type location |
|
14 val on_entry: (string * location -> unit) option -> unit |
|
15 val on_exit: (string * location -> unit) option -> unit |
|
16 val on_exit_exception: (string * location -> exn -> unit) option -> unit |
|
17 val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit |
|
18 type state |
|
19 val state: Thread.thread -> state list |
|
20 val debug_function: state -> string |
|
21 val debug_function_arg: state -> ML_Name_Space.valueVal |
|
22 val debug_function_result: state -> ML_Name_Space.valueVal |
|
23 val debug_location: state -> location |
|
24 val debug_name_space: state -> ML_Name_Space.T |
|
25 val debug_local_name_space: state -> ML_Name_Space.T |
|
26 end; |
|
27 |
|
28 structure ML_Debugger: ML_DEBUGGER = |
|
29 struct |
|
30 |
|
31 (* exceptions *) |
|
32 |
|
33 abstype exn_id = Exn_Id of string * int Unsynchronized.ref |
|
34 with |
|
35 |
|
36 fun exn_id exn = |
|
37 Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0)); |
|
38 |
|
39 fun print_exn_id (Exn_Id (name, _)) = name; |
|
40 fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2); |
|
41 |
|
42 end; |
|
43 |
|
44 val _ = |
|
45 PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id => |
|
46 let val s = print_exn_id exn_id |
|
47 in ml_pretty (ML_Pretty.String (s, size s)) end); |
|
48 |
|
49 |
|
50 (* hooks *) |
|
51 |
|
52 type location = PolyML.location; |
|
53 |
|
54 val on_entry = PolyML.DebuggerInterface.setOnEntry; |
|
55 val on_exit = PolyML.DebuggerInterface.setOnExit; |
|
56 val on_exit_exception = PolyML.DebuggerInterface.setOnExitException; |
|
57 val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint; |
|
58 |
|
59 |
|
60 (* debugger operations *) |
|
61 |
|
62 type state = PolyML.DebuggerInterface.debugState; |
|
63 |
|
64 val state = PolyML.DebuggerInterface.debugState; |
|
65 val debug_function = PolyML.DebuggerInterface.debugFunction; |
|
66 val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg; |
|
67 val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult; |
|
68 val debug_location = PolyML.DebuggerInterface.debugLocation; |
|
69 val debug_name_space = PolyML.DebuggerInterface.debugNameSpace; |
|
70 val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace; |
|
71 |
|
72 end; |