author | wenzelm |
Sat, 08 Oct 2016 22:08:31 +0200 | |
changeset 64116 | 6cfd429a4296 |
parent 63806 | c54a53ef1873 |
child 65222 | fb8253564483 |
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 |
|
61556 | 27 |
(Markup.debugger_output (Standard_Thread.the_name ())) |
60864 | 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 => |
|
62505 | 36 |
if Exn.is_interrupt exn then Exn.reraise exn |
60856 | 37 |
else error_message (Runtime.exn_message exn); |
38 |
||
60830 | 39 |
|
60888
35d85fd89fc1
eliminated cancel operation: disrupts normal evaluation of thread;
wenzelm
parents:
60887
diff
changeset
|
40 |
(* thread input *) |
60765 | 41 |
|
60888
35d85fd89fc1
eliminated cancel operation: disrupts normal evaluation of thread;
wenzelm
parents:
60887
diff
changeset
|
42 |
val thread_input = |
60891 | 43 |
Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option); |
44 |
||
45 |
fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty)); |
|
46 |
fun exit_input () = Synchronized.change thread_input (K NONE); |
|
60765 | 47 |
|
60842 | 48 |
fun input thread_name msg = |
60891 | 49 |
if null msg then error "Empty input" |
50 |
else |
|
51 |
Synchronized.change thread_input |
|
52 |
(Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg))); |
|
60887 | 53 |
|
60842 | 54 |
fun get_input thread_name = |
60891 | 55 |
Synchronized.guarded_access thread_input |
56 |
(fn NONE => SOME ([], NONE) |
|
57 |
| SOME input => |
|
58 |
(case Symtab.lookup input thread_name of |
|
59 |
NONE => NONE |
|
60 |
| SOME queue => |
|
61 |
let |
|
62 |
val (msg, queue') = Queue.dequeue queue; |
|
63 |
val input' = |
|
64 |
if Queue.is_empty queue' then Symtab.delete_safe thread_name input |
|
65 |
else Symtab.update (thread_name, queue') input; |
|
66 |
in SOME (msg, SOME input') end)); |
|
60765 | 67 |
|
68 |
||
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
69 |
(* global break *) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
70 |
|
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
71 |
local |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
72 |
val break = Synchronized.var "Debugger.break" false; |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
73 |
in |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
74 |
|
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
75 |
fun is_break () = Synchronized.value break; |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
76 |
fun set_break b = Synchronized.change break (K b); |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
77 |
|
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
78 |
end; |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
79 |
|
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
80 |
|
60869 | 81 |
|
82 |
(** thread state **) |
|
83 |
||
84 |
(* stack frame during debugging *) |
|
60856 | 85 |
|
62937 | 86 |
val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var; |
60765 | 87 |
|
62889 | 88 |
fun get_debugging () = the_default [] (Thread_Data.get debugging_var); |
60856 | 89 |
val is_debugging = not o null o get_debugging; |
60765 | 90 |
|
60856 | 91 |
fun with_debugging e = |
62937 | 92 |
Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e (); |
60749 | 93 |
|
60858 | 94 |
fun the_debug_state thread_name index = |
95 |
(case get_debugging () of |
|
96 |
[] => error ("Missing debugger information for thread " ^ quote thread_name) |
|
97 |
| states => |
|
98 |
if index < 0 orelse index >= length states then |
|
99 |
error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^ |
|
100 |
quote thread_name) |
|
101 |
else nth states index); |
|
102 |
||
103 |
||
60869 | 104 |
(* flags for single-stepping *) |
60765 | 105 |
|
60869 | 106 |
datatype stepping = Stepping of bool * int; (*stepping enabled, stack depth limit*) |
107 |
||
62889 | 108 |
val stepping_var = Thread_Data.var () : stepping Thread_Data.var; |
60869 | 109 |
|
62889 | 110 |
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var); |
111 |
fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping)); |
|
60869 | 112 |
|
113 |
fun is_stepping () = |
|
114 |
let |
|
62937 | 115 |
val stack = PolyML.DebuggerInterface.debugState (Thread.self ()); |
60869 | 116 |
val Stepping (stepping, depth) = get_stepping (); |
117 |
in stepping andalso (depth < 0 orelse length stack <= depth) end; |
|
118 |
||
60931 | 119 |
fun continue () = put_stepping (false, ~1); |
120 |
fun step () = put_stepping (true, ~1); |
|
121 |
fun step_over () = put_stepping (true, length (get_debugging ())); |
|
122 |
fun step_out () = put_stepping (true, length (get_debugging ()) - 1); |
|
60869 | 123 |
|
124 |
||
60935 | 125 |
|
60869 | 126 |
(** eval ML **) |
60765 | 127 |
|
60862 | 128 |
local |
129 |
||
130 |
val context_attempts = |
|
131 |
map ML_Lex.read |
|
62889 | 132 |
["Context.put_generic_context (SOME (Context.Theory ML_context))", |
133 |
"Context.put_generic_context (SOME (Context.Proof ML_context))", |
|
134 |
"Context.put_generic_context (SOME ML_context)"]; |
|
60862 | 135 |
|
136 |
fun evaluate {SML, verbose} = |
|
137 |
ML_Context.eval |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62891
diff
changeset
|
138 |
{SML = SML, exchange = false, redirect = false, verbose = verbose, |
60956 | 139 |
debug = SOME false, writeln = writeln_message, warning = warning_message} |
60862 | 140 |
Position.none; |
141 |
||
60935 | 142 |
fun eval_setup thread_name index SML context = |
143 |
context |
|
144 |
|> Context_Position.set_visible_generic false |
|
145 |
|> ML_Env.add_name_space {SML = SML} |
|
62937 | 146 |
(PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index)); |
60935 | 147 |
|
60897 | 148 |
fun eval_context thread_name index SML toks = |
60858 | 149 |
let |
62876 | 150 |
val context = Context.the_generic_context (); |
60897 | 151 |
val context1 = |
152 |
if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks |
|
60935 | 153 |
then context |
60862 | 154 |
else |
155 |
let |
|
60935 | 156 |
val context' = context |
157 |
|> eval_setup thread_name index SML |
|
60897 | 158 |
|> ML_Context.exec (fn () => |
159 |
evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks)); |
|
60862 | 160 |
fun try_exec toks = |
161 |
try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; |
|
162 |
in |
|
163 |
(case get_first try_exec context_attempts of |
|
164 |
SOME context2 => context2 |
|
165 |
| NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") |
|
166 |
end; |
|
60935 | 167 |
in context1 |> eval_setup thread_name index SML end; |
60897 | 168 |
|
169 |
in |
|
170 |
||
171 |
fun eval thread_name index SML txt1 txt2 = |
|
172 |
let |
|
173 |
val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
|
174 |
val context = eval_context thread_name index SML toks1; |
|
62889 | 175 |
in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end; |
60897 | 176 |
|
177 |
fun print_vals thread_name index SML txt = |
|
178 |
let |
|
60935 | 179 |
val toks = ML_Lex.read_source SML (Input.string txt) |
180 |
val context = eval_context thread_name index SML toks; |
|
62937 | 181 |
val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index); |
60897 | 182 |
|
183 |
fun print x = |
|
62663 | 184 |
Pretty.from_polyml |
62934 | 185 |
(PolyML.NameSpace.Values.printWithType |
186 |
(x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space)); |
|
60897 | 187 |
fun print_all () = |
62937 | 188 |
#allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) () |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60904
diff
changeset
|
189 |
|> sort_by #1 |> map (Pretty.item o single o print o #2) |
60897 | 190 |
|> Pretty.chunks |> Pretty.string_of |> writeln_message; |
62889 | 191 |
in Context.setmp_generic_context (SOME context) print_all () end; |
60862 | 192 |
|
193 |
end; |
|
60749 | 194 |
|
60765 | 195 |
|
60869 | 196 |
|
60891 | 197 |
(** debugger loop **) |
60857 | 198 |
|
199 |
local |
|
60765 | 200 |
|
60842 | 201 |
fun debugger_state thread_name = |
202 |
Output.protocol_message (Markup.debugger_state thread_name) |
|
60856 | 203 |
[get_debugging () |
60842 | 204 |
|> map (fn st => |
62821 | 205 |
(Position.properties_of |
62937 | 206 |
(Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)), |
207 |
PolyML.DebuggerInterface.debugFunction st)) |
|
60842 | 208 |
|> let open XML.Encode in list (pair properties string) end |
209 |
|> YXML.string_of_body]; |
|
210 |
||
60857 | 211 |
fun debugger_command thread_name = |
212 |
(case get_input thread_name of |
|
60931 | 213 |
[] => (continue (); false) |
214 |
| ["continue"] => (continue (); false) |
|
215 |
| ["step"] => (step (); false) |
|
216 |
| ["step_over"] => (step_over (); false) |
|
217 |
| ["step_out"] => (step_out (); false) |
|
60857 | 218 |
| ["eval", index, SML, txt1, txt2] => |
219 |
(error_wrapper (fn () => |
|
63806 | 220 |
eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true) |
60897 | 221 |
| ["print_vals", index, SML, txt] => |
222 |
(error_wrapper (fn () => |
|
63806 | 223 |
print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true) |
60857 | 224 |
| bad => |
225 |
(Output.system_message |
|
226 |
("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); |
|
227 |
||
60889 | 228 |
in |
229 |
||
60842 | 230 |
fun debugger_loop thread_name = |
62923 | 231 |
Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
60885
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
232 |
let |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
233 |
fun loop () = |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
234 |
(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
|
235 |
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
|
236 |
val _ = debugger_state thread_name; |
d8d51f956f05
report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents:
60884
diff
changeset
|
237 |
in Exn.release result end) (); |
60765 | 238 |
|
60857 | 239 |
end; |
240 |
||
60765 | 241 |
|
60869 | 242 |
|
243 |
(** protocol commands **) |
|
60765 | 244 |
|
245 |
val _ = |
|
246 |
Isabelle_Process.protocol_command "Debugger.init" |
|
60889 | 247 |
(fn [] => |
60891 | 248 |
(init_input (); |
62937 | 249 |
PolyML.DebuggerInterface.setOnBreakPoint |
60889 | 250 |
(SOME (fn (_, break) => |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
251 |
if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ()) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
252 |
then |
61556 | 253 |
(case Standard_Thread.get_name () of |
60889 | 254 |
SOME thread_name => debugger_loop thread_name |
255 |
| NONE => ()) |
|
60891 | 256 |
else ())))); |
60889 | 257 |
|
258 |
val _ = |
|
259 |
Isabelle_Process.protocol_command "Debugger.exit" |
|
62937 | 260 |
(fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ())); |
60765 | 261 |
|
262 |
val _ = |
|
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
263 |
Isabelle_Process.protocol_command "Debugger.break" |
63806 | 264 |
(fn [b] => set_break (Value.parse_bool b)); |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
265 |
|
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60931
diff
changeset
|
266 |
val _ = |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
267 |
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
|
268 |
(fn [node_name, id0, breakpoint0, breakpoint_state0] => |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
269 |
let |
63806 | 270 |
val id = Value.parse_int id0; |
271 |
val breakpoint = Value.parse_int breakpoint0; |
|
272 |
val breakpoint_state = Value.parse_bool breakpoint_state0; |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
273 |
|
63806 | 274 |
fun err () = error ("Bad exec for command " ^ Value.print_int id); |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
275 |
in |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
276 |
(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
|
277 |
SOME (eval, _) => |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
278 |
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
|
279 |
let |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
in |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
284 |
(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
|
285 |
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
|
286 |
| NONE => err ()) |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
287 |
end |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
288 |
else err () |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
289 |
| NONE => err ()) |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
290 |
end); |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
291 |
|
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60871
diff
changeset
|
292 |
val _ = |
60765 | 293 |
Isabelle_Process.protocol_command "Debugger.input" |
60842 | 294 |
(fn thread_name :: msg => input thread_name msg); |
60765 | 295 |
|
60749 | 296 |
end; |