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 |
|
60830
|
17 |
(* messages *)
|
|
18 |
|
60834
|
19 |
fun output_message kind msg =
|
60830
|
20 |
Output.protocol_message
|
60834
|
21 |
(Markup.debugger_output (Simple_Thread.the_name ()))
|
|
22 |
[Markup.markup (kind, Markup.serial_properties (serial ())) msg];
|
|
23 |
|
|
24 |
val writeln_message = output_message Markup.writelnN;
|
|
25 |
val warning_message = output_message Markup.warningN;
|
|
26 |
val error_message = output_message Markup.errorN;
|
60830
|
27 |
|
|
28 |
|
60765
|
29 |
(* global state *)
|
|
30 |
|
|
31 |
datatype state =
|
|
32 |
State of {
|
60829
|
33 |
threads: Thread.thread Symtab.table, (*thread name ~> thread*)
|
|
34 |
input: string list Queue.T Symtab.table (*thread name ~> input queue*)
|
60765
|
35 |
};
|
|
36 |
|
|
37 |
fun make_state (threads, input) = State {threads = threads, input = input};
|
|
38 |
val init_state = make_state (Symtab.empty, Symtab.empty);
|
|
39 |
fun map_state f (State {threads, input}) = make_state (f (threads, input));
|
|
40 |
|
|
41 |
val global_state = Synchronized.var "Debugger.state" init_state;
|
|
42 |
|
60842
|
43 |
fun cancel thread_name =
|
60765
|
44 |
Synchronized.change global_state (tap (fn State {threads, ...} =>
|
60842
|
45 |
(case Symtab.lookup threads thread_name of
|
60765
|
46 |
NONE => ()
|
|
47 |
| SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
|
|
48 |
|
60842
|
49 |
fun input thread_name msg =
|
60765
|
50 |
Synchronized.change global_state (map_state (fn (threads, input) =>
|
60842
|
51 |
let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
|
60765
|
52 |
in (threads, input') end));
|
|
53 |
|
60842
|
54 |
fun get_input thread_name =
|
60765
|
55 |
Synchronized.guarded_access global_state (fn State {threads, input} =>
|
60842
|
56 |
(case Symtab.lookup input thread_name of
|
60765
|
57 |
NONE => NONE
|
|
58 |
| SOME queue =>
|
|
59 |
let
|
|
60 |
val (msg, queue') = Queue.dequeue queue;
|
|
61 |
val input' =
|
60842
|
62 |
if Queue.is_empty queue' then Symtab.delete_safe thread_name input
|
|
63 |
else Symtab.update (thread_name, queue') input;
|
60765
|
64 |
in SOME (msg, make_state (threads, input')) end));
|
|
65 |
|
|
66 |
|
|
67 |
(* thread data *)
|
|
68 |
|
|
69 |
local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
|
|
70 |
|
|
71 |
fun get_data () = the_default [] (Thread.getLocal tag);
|
|
72 |
fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
|
|
73 |
|
60749
|
74 |
end;
|
|
75 |
|
60765
|
76 |
val debugging = not o null o get_data;
|
|
77 |
fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
|
|
78 |
|
|
79 |
|
|
80 |
(* protocol messages *)
|
60749
|
81 |
|
|
82 |
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
|
|
83 |
|
60765
|
84 |
|
|
85 |
(* main entry point *)
|
|
86 |
|
60842
|
87 |
fun debugger_state thread_name =
|
|
88 |
Output.protocol_message (Markup.debugger_state thread_name)
|
|
89 |
[get_data ()
|
|
90 |
|> map (fn st =>
|
|
91 |
(Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
|
|
92 |
ML_Debugger.debug_function st))
|
|
93 |
|> let open XML.Encode in list (pair properties string) end
|
|
94 |
|> YXML.string_of_body];
|
|
95 |
|
|
96 |
fun debugger_loop thread_name =
|
|
97 |
(debugger_state thread_name;
|
|
98 |
case get_input thread_name of
|
60765
|
99 |
["continue"] => ()
|
|
100 |
| bad =>
|
|
101 |
(Output.system_message
|
|
102 |
("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
|
60842
|
103 |
debugger_loop thread_name));
|
60765
|
104 |
|
|
105 |
fun debugger cond =
|
|
106 |
if debugging () orelse not (cond ()) orelse
|
|
107 |
not (Options.default_bool @{system_option ML_debugger_active})
|
|
108 |
then ()
|
|
109 |
else
|
|
110 |
with_debugging (fn () =>
|
60830
|
111 |
(case Simple_Thread.get_name () of
|
60765
|
112 |
NONE => ()
|
60842
|
113 |
| SOME thread_name => debugger_loop thread_name));
|
60765
|
114 |
|
|
115 |
fun init () =
|
|
116 |
ML_Debugger.on_breakpoint
|
|
117 |
(SOME (fn (_, b) =>
|
|
118 |
debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
|
|
119 |
|
|
120 |
|
|
121 |
(* protocol commands *)
|
|
122 |
|
|
123 |
val _ =
|
|
124 |
Isabelle_Process.protocol_command "Debugger.init"
|
|
125 |
(fn [] => init ());
|
|
126 |
|
|
127 |
val _ =
|
|
128 |
Isabelle_Process.protocol_command "Debugger.cancel"
|
60842
|
129 |
(fn [thread_name] => cancel thread_name);
|
60765
|
130 |
|
|
131 |
val _ =
|
|
132 |
Isabelle_Process.protocol_command "Debugger.input"
|
60842
|
133 |
(fn thread_name :: msg => input thread_name msg);
|
60765
|
134 |
|
60749
|
135 |
end;
|