9 |
9 |
10 (* global state *) |
10 (* global state *) |
11 |
11 |
12 datatype state = |
12 datatype state = |
13 State of { |
13 State of { |
14 threads: Thread.thread Symtab.table, (*thread identification ~> thread*) |
14 threads: Thread.thread Symtab.table, (*thread name ~> thread*) |
15 input: string list Queue.T Symtab.table (*thread identification ~> input queue*) |
15 input: string list Queue.T Symtab.table (*thread name ~> input queue*) |
16 }; |
16 }; |
17 |
17 |
18 fun make_state (threads, input) = State {threads = threads, input = input}; |
18 fun make_state (threads, input) = State {threads = threads, input = input}; |
19 val init_state = make_state (Symtab.empty, Symtab.empty); |
19 val init_state = make_state (Symtab.empty, Symtab.empty); |
20 fun map_state f (State {threads, input}) = make_state (f (threads, input)); |
20 fun map_state f (State {threads, input}) = make_state (f (threads, input)); |
21 |
21 |
22 val global_state = Synchronized.var "Debugger.state" init_state; |
22 val global_state = Synchronized.var "Debugger.state" init_state; |
23 |
23 |
24 fun cancel id = |
24 fun cancel name = |
25 Synchronized.change global_state (tap (fn State {threads, ...} => |
25 Synchronized.change global_state (tap (fn State {threads, ...} => |
26 (case Symtab.lookup threads id of |
26 (case Symtab.lookup threads name of |
27 NONE => () |
27 NONE => () |
28 | SOME thread => Simple_Thread.interrupt_unsynchronized thread))); |
28 | SOME thread => Simple_Thread.interrupt_unsynchronized thread))); |
29 |
29 |
30 fun input id msg = |
30 fun input name msg = |
31 Synchronized.change global_state (map_state (fn (threads, input) => |
31 Synchronized.change global_state (map_state (fn (threads, input) => |
32 let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input; |
32 let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input; |
33 in (threads, input') end)); |
33 in (threads, input') end)); |
34 |
34 |
35 fun get_input id = |
35 fun get_input name = |
36 Synchronized.guarded_access global_state (fn State {threads, input} => |
36 Synchronized.guarded_access global_state (fn State {threads, input} => |
37 (case Symtab.lookup input id of |
37 (case Symtab.lookup input name of |
38 NONE => NONE |
38 NONE => NONE |
39 | SOME queue => |
39 | SOME queue => |
40 let |
40 let |
41 val (msg, queue') = Queue.dequeue queue; |
41 val (msg, queue') = Queue.dequeue queue; |
42 val input' = |
42 val input' = |
43 if Queue.is_empty queue' then Symtab.delete_safe id input |
43 if Queue.is_empty queue' then Symtab.delete_safe name input |
44 else Symtab.update (id, queue') input; |
44 else Symtab.update (name, queue') input; |
45 in SOME (msg, make_state (threads, input')) end)); |
45 in SOME (msg, make_state (threads, input')) end)); |
46 |
46 |
47 |
47 |
48 (* thread data *) |
48 (* thread data *) |
49 |
49 |
63 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
63 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
64 |
64 |
65 |
65 |
66 (* main entry point *) |
66 (* main entry point *) |
67 |
67 |
68 fun debug_loop id = |
68 fun debug_loop name = |
69 (case get_input id of |
69 (case get_input name of |
70 ["continue"] => () |
70 ["continue"] => () |
71 | bad => |
71 | bad => |
72 (Output.system_message |
72 (Output.system_message |
73 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); |
73 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); |
74 debug_loop id)); |
74 debug_loop name)); |
75 |
75 |
76 fun debugger cond = |
76 fun debugger cond = |
77 if debugging () orelse not (cond ()) orelse |
77 if debugging () orelse not (cond ()) orelse |
78 not (Options.default_bool @{system_option ML_debugger_active}) |
78 not (Options.default_bool @{system_option ML_debugger_active}) |
79 then () |
79 then () |
80 else |
80 else |
81 with_debugging (fn () => |
81 with_debugging (fn () => |
82 (case Simple_Thread.identification () of |
82 (case Simple_Thread.name () of |
83 NONE => () |
83 NONE => () |
84 | SOME id => debug_loop id)); |
84 | SOME name => debug_loop name)); |
85 |
85 |
86 fun init () = |
86 fun init () = |
87 ML_Debugger.on_breakpoint |
87 ML_Debugger.on_breakpoint |
88 (SOME (fn (_, b) => |
88 (SOME (fn (_, b) => |
89 debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping}))); |
89 debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping}))); |