author | wenzelm |
Thu, 06 Aug 2015 11:46:47 +0200 | |
changeset 60852 | 1c51a2ca8204 |
parent 60745 | d86b4cd0f1ec |
child 60853 | b0627cb2e08d |
permissions | -rw-r--r-- |
60745
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60744
diff
changeset
|
1 |
(* Title: Pure/ML/ml_debugger.ML |
60729 | 2 |
Author: Makarius |
3 |
||
60745
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60744
diff
changeset
|
4 |
ML debugger interface. |
60729 | 5 |
*) |
6 |
||
7 |
signature ML_DEBUGGER = |
|
8 |
sig |
|
60852
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
9 |
val on_entry: (string * 'a -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
10 |
val on_exit: (string * 'a -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
11 |
val on_exit_exception: (string * 'a -> exn -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
12 |
val on_breakpoint: ('a * bool Unsynchronized.ref -> unit) option -> unit |
60729 | 13 |
type state |
14 |
val state: Thread.thread -> state list |
|
15 |
val debug_function: state -> string |
|
16 |
val debug_function_arg: state -> ML_Name_Space.valueVal |
|
17 |
val debug_function_result: state -> ML_Name_Space.valueVal |
|
60852
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
18 |
val debug_location: state -> 'a |
60729 | 19 |
val debug_name_space: state -> ML_Name_Space.T |
20 |
end; |
|
21 |
||
22 |
structure ML_Debugger: ML_DEBUGGER = |
|
23 |
struct |
|
24 |
||
25 |
(* hooks *) |
|
26 |
||
27 |
type location = unit; |
|
28 |
fun on_entry _ = (); |
|
29 |
fun on_exit _ = (); |
|
30 |
fun on_exit_exception _ = (); |
|
60744 | 31 |
fun on_breakpoint _ = (); |
60729 | 32 |
|
33 |
||
34 |
(* debugger *) |
|
35 |
||
36 |
fun fail () = raise Fail "No debugger support on this ML platform"; |
|
37 |
||
38 |
type state = unit; |
|
39 |
||
40 |
fun state _ = []; |
|
41 |
fun debug_function () = fail (); |
|
42 |
fun debug_function_arg () = fail (); |
|
43 |
fun debug_function_result () = fail (); |
|
44 |
fun debug_location () = fail (); |
|
45 |
fun debug_name_space () = fail (); |
|
46 |
||
47 |
end; |