author | wenzelm |
Mon, 10 Aug 2015 22:21:55 +0200 | |
changeset 60885 | d8d51f956f05 |
parent 60884 | f3039309702e |
child 60887 | 9d8b244234ab |
permissions | -rw-r--r-- |
60749 | 1 |
(* Title: Pure/Tools/debugger.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Interactive debugger for Isabelle/ML. |
|
5 |
*) |
|
6 |
||
60830 | 7 |
signature DEBUGGER = |
8 |
sig |
|
60834 | 9 |
val writeln_message: string -> unit |
10 |
val warning_message: string -> unit |
|
11 |
val error_message: string -> unit |
|
60830 | 12 |
end; |
13 |
||
14 |
structure Debugger: DEBUGGER = |
|
60765 | 15 |
struct |
16 |
||
60869 | 17 |
(** global state **) |
18 |
||
19 |
(* output messages *) |
|
60830 | 20 |
|
60856 | 21 |
val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
22 |
||
60834 | 23 |
fun output_message kind msg = |
60864 | 24 |
if msg = "" then () |
25 |
else |
|
26 |
Output.protocol_message |
|
27 |
(Markup.debugger_output (Simple_Thread.the_name ())) |
|
28 |
[Markup.markup (kind, Markup.serial_properties (serial ())) msg]; |
|
60834 | 29 |
|
30 |
val writeln_message = output_message Markup.writelnN; |
|
31 |
val warning_message = output_message Markup.warningN; |
|
32 |
val error_message = output_message Markup.errorN; |
|
60830 | 33 |
|
60856 | 34 |
fun error_wrapper e = e () |
35 |
handle exn => |
|
36 |
if Exn.is_interrupt exn then reraise exn |
|
37 |
else error_message (Runtime.exn_message exn); |
|
38 |
||
60830 | 39 |
|
60869 | 40 |
(* thread names and input *) |
60765 | 41 |
|
42 |
datatype state = |
|
43 |
State of { |
|
60829 | 44 |
threads: Thread.thread Symtab.table, (*thread name ~> thread*) |
45 |
input: string list Queue.T Symtab.table (*thread name ~> input queue*) |
|
60765 | 46 |
}; |
47 |
||
48 |
fun make_state (threads, input) = State {threads = threads, input = input}; |
|
49 |
val init_state = make_state (Symtab.empty, Symtab.empty); |
|
50 |
fun map_state f (State {threads, input}) = make_state (f (threads, input)); |
|
51 |
||
52 |
val global_state = Synchronized.var "Debugger.state" init_state; |
|
53 |
||
60842 | 54 |
fun cancel thread_name = |
60765 | 55 |
Synchronized.change global_state (tap (fn State {threads, ...} => |
60842 | 56 |
(case Symtab.lookup threads thread_name of |
60765 | 57 |
NONE => () |
58 |
| SOME thread => Simple_Thread.interrupt_unsynchronized thread))); |
|
59 |
||
60842 | 60 |
fun input thread_name msg = |
60765 | 61 |
Synchronized.change global_state (map_state (fn (threads, input) => |
60842 | 62 |
let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input; |
60765 | 63 |
in (threads, input') end)); |
64 |
||
60842 | 65 |
fun get_input thread_name = |
60765 | 66 |
Synchronized.guarded_access global_state (fn State {threads, input} => |
60842 | 67 |
(case Symtab.lookup input thread_name of |
60765 | 68 |
NONE => NONE |
69 |
| SOME queue => |
|
70 |
let |
|
71 |
val (msg, queue') = Queue.dequeue queue; |
|
72 |
val input' = |
|
60842 | 73 |
if Queue.is_empty queue' then Symtab.delete_safe thread_name input |
74 |
else Symtab.update (thread_name, queue') input; |
|
60765 | 75 |
in SOME (msg, make_state (threads, input')) end)); |
76 |
||
77 |
||
60869 | 78 |
|
79 |
(** thread state **) |
|
80 |
||
81 |
(* stack frame during debugging *) |
|
60856 | 82 |
|
83 |
local |
|
84 |
val tag = Universal.tag () : ML_Debugger.state list Universal.tag; |
|
85 |
in |
|
60765 | 86 |
|
60856 | 87 |
fun get_debugging () = the_default [] (Thread.getLocal tag); |
88 |
val is_debugging = not o null o get_debugging; |
|
60765 | 89 |
|
60856 | 90 |
fun with_debugging e = |
91 |
setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e (); |
|
60765 | 92 |
|
60749 | 93 |
end; |
94 |
||
60858 | 95 |
fun the_debug_state thread_name index = |
96 |
(case get_debugging () of |
|
97 |
[] => error ("Missing debugger information for thread " ^ quote thread_name) |
|
98 |
| states => |
|
99 |
if index < 0 orelse index >= length states then |
|
100 |
error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^ |
|
101 |
quote thread_name) |
|
102 |
else nth states index); |
|
103 |
||
104 |
||
60869 | 105 |
(* flags for single-stepping *) |
60765 | 106 |
|
60869 | 107 |
datatype stepping = Stepping of bool * int; (*stepping enabled, stack depth limit*) |
108 |
||
109 |
local |
|
110 |
val tag = Universal.tag () : stepping Universal.tag; |
|
111 |
in |
|
112 |
||
113 |
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag); |
|
114 |
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping); |
|
115 |
||
116 |
end; |
|
117 |
||
118 |
fun is_stepping () = |
|
119 |
let |
|
120 |
val stack = ML_Debugger.state (Thread.self ()); |
|
121 |
val Stepping (stepping, depth) = get_stepping (); |
|
122 |
in stepping andalso (depth < 0 orelse length stack <= depth) end; |
|
123 |
||
124 |
fun step_stepping () = put_stepping (true, ~1); |
|
125 |
fun step_over_stepping () = put_stepping (true, length (get_debugging ())); |
|
126 |
fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1); |
|
127 |
fun continue_stepping () = put_stepping (false, ~1); |
|
128 |
||
129 |
||
130 |
(** eval ML **) |
|
60765 | 131 |
|
60862 | 132 |
local |
133 |
||
134 |
val context_attempts = |
|
135 |
map ML_Lex.read |
|
136 |
["Context.set_thread_data (SOME (Context.Theory ML_context))", |
|
137 |
"Context.set_thread_data (SOME (Context.Proof ML_context))", |
|
138 |
"Context.set_thread_data (SOME ML_context)"]; |
|
139 |
||
140 |
fun evaluate {SML, verbose} = |
|
141 |
ML_Context.eval |
|
142 |
{SML = SML, exchange = false, redirect = false, verbose = verbose, |
|
143 |
writeln = writeln_message, warning = warning_message} |
|
144 |
Position.none; |
|
145 |
||
146 |
in |
|
147 |
||
60858 | 148 |
fun eval thread_name index SML txt1 txt2 = |
149 |
let |
|
60862 | 150 |
val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
60858 | 151 |
|
60862 | 152 |
val evaluate_verbose = evaluate {SML = SML, verbose = true}; |
60858 | 153 |
val context1 = ML_Context.the_generic_context () |
154 |
|> Context_Position.set_visible_generic false |
|
60871 | 155 |
|> Config.put_generic ML_Options.debugger false |
60862 | 156 |
|> ML_Env.add_name_space {SML = SML} |
157 |
(ML_Debugger.debug_name_space (the_debug_state thread_name index)); |
|
158 |
val context2 = |
|
159 |
if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1 |
|
160 |
then context1 |
|
161 |
else |
|
162 |
let |
|
163 |
val context' = context1 |
|
164 |
|> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1)); |
|
165 |
fun try_exec toks = |
|
166 |
try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; |
|
167 |
in |
|
168 |
(case get_first try_exec context_attempts of |
|
169 |
SOME context2 => context2 |
|
170 |
| NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") |
|
171 |
end; |
|
172 |
in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end; |
|
173 |
||
174 |
end; |
|
60749 | 175 |
|
60765 | 176 |
|
60869 | 177 |
|
178 |
(** debugger entry point **) |
|
60857 | 179 |
|
180 |
local |
|
60765 | 181 |
|
60842 | 182 |
fun debugger_state thread_name = |
183 |
Output.protocol_message (Markup.debugger_state thread_name) |
|
60856 | 184 |
[get_debugging () |
60842 | 185 |
|> map (fn st => |
186 |
(Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)), |
|
187 |
ML_Debugger.debug_function st)) |
|
188 |
|> let open XML.Encode in list (pair properties string) end |
|
189 |
|> YXML.string_of_body]; |
|
190 |
||
60857 | 191 |
fun debugger_command thread_name = |
192 |
(case get_input thread_name of |
|
60869 | 193 |
["step"] => (step_stepping (); false) |
194 |
| ["step_over"] => (step_over_stepping (); false) |
|
195 |
| ["step_out"] => (step_out_stepping (); false) |
|
196 |
| ["continue"] => (continue_stepping (); false) |
|
60857 | 197 |
| ["eval", index, SML, txt1, txt2] => |
198 |
(error_wrapper (fn () => |
|
199 |
eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true) |
|
200 |
| bad => |
|
201 |
(Output.system_message |
|
202 |
("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); |
|
203 |
||
60842 | 204 |
fun debugger_loop thread_name = |
60885
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
205 |
uninterruptible (fn restore_attributes => fn () => |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
206 |
let |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
207 |
fun loop () = |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
208 |
(debugger_state thread_name; if debugger_command thread_name then loop () else ()); |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
209 |
val result = Exn.capture (restore_attributes with_debugging) loop; |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
210 |
val _ = debugger_state thread_name; |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
211 |
in Exn.release result end) (); |
60765 | 212 |
|
60857 | 213 |
in |
214 |
||
60765 | 215 |
fun init () = |
216 |
ML_Debugger.on_breakpoint |
|
60869 | 217 |
(SOME (fn (_, break) => |
218 |
if not (is_debugging ()) andalso |
|
60884
f3039309702e
eliminated global option: breakpoints control this individually;
wenzelm
parents:
60880
diff
changeset
|
219 |
(! break orelse is_stepping ()) andalso |
60869 | 220 |
Options.default_bool @{system_option ML_debugger_active} |
221 |
then |
|
222 |
(case Simple_Thread.get_name () of |
|
223 |
SOME thread_name => debugger_loop thread_name |
|
224 |
| NONE => ()) |
|
225 |
else ())); |
|
60765 | 226 |
|
60857 | 227 |
end; |
228 |
||
60765 | 229 |
|
60869 | 230 |
|
231 |
(** protocol commands **) |
|
60765 | 232 |
|
233 |
val _ = |
|
234 |
Isabelle_Process.protocol_command "Debugger.init" |
|
235 |
(fn [] => init ()); |
|
236 |
||
237 |
val _ = |
|
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
238 |
Isabelle_Process.protocol_command "Debugger.breakpoint" |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
239 |
(fn [node_name, id0, breakpoint0, breakpoint_state0] => |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
240 |
let |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
241 |
val id = Markup.parse_int id0; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
242 |
val breakpoint = Markup.parse_int breakpoint0; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
243 |
val breakpoint_state = Markup.parse_bool breakpoint_state0; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
244 |
|
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
245 |
fun err () = error ("Bad exec for command " ^ Markup.print_int id); |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
246 |
in |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
247 |
(case Document.command_exec (Document.state ()) node_name id of |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
248 |
SOME (eval, _) => |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
249 |
if Command.eval_finished eval then |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
250 |
let |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
251 |
val st = Command.eval_result_state eval; |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
252 |
val ctxt = Toplevel.presentation_context_of st |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
253 |
handle Toplevel.UNDEF => err (); |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
254 |
in |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
255 |
(case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
256 |
SOME (b, _) => b := breakpoint_state |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
257 |
| NONE => err ()) |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
258 |
end |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
259 |
else err () |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
260 |
| NONE => err ()) |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
261 |
end); |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
262 |
|
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
263 |
val _ = |
60765 | 264 |
Isabelle_Process.protocol_command "Debugger.cancel" |
60842 | 265 |
(fn [thread_name] => cancel thread_name); |
60765 | 266 |
|
267 |
val _ = |
|
268 |
Isabelle_Process.protocol_command "Debugger.input" |
|
60842 | 269 |
(fn thread_name :: msg => input thread_name msg); |
60765 | 270 |
|
60749 | 271 |
end; |