equal
deleted
inserted
replaced
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Interactive debugger for Isabelle/ML. |
4 Interactive debugger for Isabelle/ML. |
5 *) |
5 *) |
6 |
6 |
7 structure Debugger: sig end = |
7 signature DEBUGGER = |
|
8 sig |
|
9 val output: string -> unit |
|
10 end; |
|
11 |
|
12 structure Debugger: DEBUGGER = |
8 struct |
13 struct |
|
14 |
|
15 (* messages *) |
|
16 |
|
17 fun output msg = |
|
18 Output.protocol_message |
|
19 (Markup.debugger_output (Simple_Thread.the_name ()) (serial ())) [msg]; |
|
20 |
9 |
21 |
10 (* global state *) |
22 (* global state *) |
11 |
23 |
12 datatype state = |
24 datatype state = |
13 State of { |
25 State of { |
77 if debugging () orelse not (cond ()) orelse |
89 if debugging () orelse not (cond ()) orelse |
78 not (Options.default_bool @{system_option ML_debugger_active}) |
90 not (Options.default_bool @{system_option ML_debugger_active}) |
79 then () |
91 then () |
80 else |
92 else |
81 with_debugging (fn () => |
93 with_debugging (fn () => |
82 (case Simple_Thread.name () of |
94 (case Simple_Thread.get_name () of |
83 NONE => () |
95 NONE => () |
84 | SOME name => debug_loop name)); |
96 | SOME name => debug_loop name)); |
85 |
97 |
86 fun init () = |
98 fun init () = |
87 ML_Debugger.on_breakpoint |
99 ML_Debugger.on_breakpoint |