author | wenzelm |
Thu, 03 Mar 2016 11:12:02 +0100 | |
changeset 62501 | 98fa1f9a292f |
parent 62387 | src/Pure/RAW/ml_debugger_polyml-5.6.ML@ad3eb2889f9a |
child 62503 | 19afb533028e |
permissions | -rw-r--r-- |
62501 | 1 |
(* Title: Pure/RAW/ml_debugger.ML |
60729 | 2 |
Author: Makarius |
3 |
||
61794
4c232a2ddeab
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
wenzelm
parents:
60954
diff
changeset
|
4 |
ML debugger interface -- for Poly/ML 5.6, or later. |
60729 | 5 |
*) |
6 |
||
60852
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
7 |
signature ML_DEBUGGER = |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
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 |
60852
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
13 |
type location |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
14 |
val on_entry: (string * location -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
15 |
val on_exit: (string * location -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
16 |
val on_exit_exception: (string * location -> exn -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
17 |
val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
18 |
type state |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
19 |
val state: Thread.thread -> state list |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
20 |
val debug_function: state -> string |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
21 |
val debug_function_arg: state -> ML_Name_Space.valueVal |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
22 |
val debug_function_result: state -> ML_Name_Space.valueVal |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
23 |
val debug_location: state -> location |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
24 |
val debug_name_space: state -> ML_Name_Space.T |
61886 | 25 |
val debug_local_name_space: state -> ML_Name_Space.T |
60852
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
26 |
end; |
1c51a2ca8204
clarified signature, to make debugger.ML compile with current official ML versions;
wenzelm
parents:
60745
diff
changeset
|
27 |
|
60729 | 28 |
structure ML_Debugger: ML_DEBUGGER = |
29 |
struct |
|
30 |
||
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
|
31 |
(* 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
|
32 |
|
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 |
abstype exn_id = Exn_Id of string * int Unsynchronized.ref |
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 |
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
|
35 |
|
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 exn_id 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
|
37 |
Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0)); |
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 |
|
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 |
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
|
40 |
fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2); |
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
|
41 |
|
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
|
42 |
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
|
43 |
|
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
|
44 |
val _ = |
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
|
45 |
PolyML.addPrettyPrinter (fn _ => fn _ => fn 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
|
46 |
let val s = print_exn_id exn_id |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
47 |
in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end); |
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
|
48 |
|
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
|
49 |
|
60729 | 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; |
|
60744 | 57 |
val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint; |
60729 | 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; |
|
61886 | 70 |
val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace; |
60729 | 71 |
|
72 |
end; |