author | blanchet |
Fri, 02 Oct 2015 21:06:32 +0200 | |
changeset 61310 | 9a50ea544fd3 |
parent 60954 | eeee8349e9eb |
child 61886 | 5a9a85c4cfb3 |
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 |
||
60853 | 4 |
ML debugger interface -- dummy version. |
60729 | 5 |
*) |
6 |
||
7 |
signature ML_DEBUGGER = |
|
8 |
sig |
|
60954
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
9 |
type exn_id |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
10 |
val exn_id: exn -> exn_id |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
11 |
val print_exn_id: exn_id -> string |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
12 |
val eq_exn_id: exn_id * exn_id -> bool |
60853 | 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 |
|
60729 | 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 |
|
60853 | 22 |
val debug_location: state -> 'location |
60729 | 23 |
val debug_name_space: state -> ML_Name_Space.T |
24 |
end; |
|
25 |
||
26 |
structure ML_Debugger: ML_DEBUGGER = |
|
27 |
struct |
|
28 |
||
60954
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
29 |
(* exceptions *) |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
30 |
|
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
31 |
abstype exn_id = Exn_Id of string |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
32 |
with |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
33 |
|
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
34 |
fun exn_id exn = Exn_Id (General.exnName exn); |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
35 |
fun print_exn_id (Exn_Id name) = name; |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
36 |
fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2; (*over-approximation*) |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
37 |
|
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
38 |
end; |
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
39 |
|
eeee8349e9eb
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
wenzelm
parents:
60853
diff
changeset
|
40 |
|
60729 | 41 |
(* hooks *) |
42 |
||
43 |
fun on_entry _ = (); |
|
44 |
fun on_exit _ = (); |
|
45 |
fun on_exit_exception _ = (); |
|
60744 | 46 |
fun on_breakpoint _ = (); |
60729 | 47 |
|
48 |
||
49 |
(* debugger *) |
|
50 |
||
51 |
fun fail () = raise Fail "No debugger support on this ML platform"; |
|
52 |
||
53 |
type state = unit; |
|
54 |
||
55 |
fun state _ = []; |
|
56 |
fun debug_function () = fail (); |
|
57 |
fun debug_function_arg () = fail (); |
|
58 |
fun debug_function_result () = fail (); |
|
59 |
fun debug_location () = fail (); |
|
60 |
fun debug_name_space () = fail (); |
|
61 |
||
62 |
end; |