14 structure Debugger: DEBUGGER = |
14 structure Debugger: DEBUGGER = |
15 struct |
15 struct |
16 |
16 |
17 (* messages *) |
17 (* messages *) |
18 |
18 |
|
19 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
|
20 |
19 fun output_message kind msg = |
21 fun output_message kind msg = |
20 Output.protocol_message |
22 Output.protocol_message |
21 (Markup.debugger_output (Simple_Thread.the_name ())) |
23 (Markup.debugger_output (Simple_Thread.the_name ())) |
22 [Markup.markup (kind, Markup.serial_properties (serial ())) msg]; |
24 [Markup.markup (kind, Markup.serial_properties (serial ())) msg]; |
23 |
25 |
24 val writeln_message = output_message Markup.writelnN; |
26 val writeln_message = output_message Markup.writelnN; |
25 val warning_message = output_message Markup.warningN; |
27 val warning_message = output_message Markup.warningN; |
26 val error_message = output_message Markup.errorN; |
28 val error_message = output_message Markup.errorN; |
|
29 |
|
30 fun error_wrapper e = e () |
|
31 handle exn => |
|
32 if Exn.is_interrupt exn then reraise exn |
|
33 else error_message (Runtime.exn_message exn); |
27 |
34 |
28 |
35 |
29 (* global state *) |
36 (* global state *) |
30 |
37 |
31 datatype state = |
38 datatype state = |
62 if Queue.is_empty queue' then Symtab.delete_safe thread_name input |
69 if Queue.is_empty queue' then Symtab.delete_safe thread_name input |
63 else Symtab.update (thread_name, queue') input; |
70 else Symtab.update (thread_name, queue') input; |
64 in SOME (msg, make_state (threads, input')) end)); |
71 in SOME (msg, make_state (threads, input')) end)); |
65 |
72 |
66 |
73 |
67 (* thread data *) |
74 (* thread state *) |
68 |
75 |
69 local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in |
76 local |
|
77 val tag = Universal.tag () : ML_Debugger.state list Universal.tag; |
|
78 in |
70 |
79 |
71 fun get_data () = the_default [] (Thread.getLocal tag); |
80 fun get_debugging () = the_default [] (Thread.getLocal tag); |
72 fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x; |
81 val is_debugging = not o null o get_debugging; |
|
82 |
|
83 fun with_debugging e = |
|
84 setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e (); |
73 |
85 |
74 end; |
86 end; |
75 |
87 |
76 val debugging = not o null o get_data; |
|
77 fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e (); |
|
78 |
88 |
|
89 (* eval ML *) |
79 |
90 |
80 (* protocol messages *) |
91 fun eval opt_index SML context expression = (* FIXME *) |
81 |
92 writeln_message ("context = " ^ context ^ "\nexpression = " ^ expression); |
82 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
|
83 |
93 |
84 |
94 |
85 (* main entry point *) |
95 (* main entry point *) |
86 |
96 |
87 fun debugger_state thread_name = |
97 fun debugger_state thread_name = |
88 Output.protocol_message (Markup.debugger_state thread_name) |
98 Output.protocol_message (Markup.debugger_state thread_name) |
89 [get_data () |
99 [get_debugging () |
90 |> map (fn st => |
100 |> map (fn st => |
91 (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)), |
101 (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)), |
92 ML_Debugger.debug_function st)) |
102 ML_Debugger.debug_function st)) |
93 |> let open XML.Encode in list (pair properties string) end |
103 |> let open XML.Encode in list (pair properties string) end |
94 |> YXML.string_of_body]; |
104 |> YXML.string_of_body]; |
95 |
105 |
96 fun debugger_loop thread_name = |
106 fun debugger_loop thread_name = |
97 (debugger_state thread_name; |
107 let |
98 case get_input thread_name of |
108 fun loop () = |
99 ["continue"] => () |
109 (debugger_state thread_name; |
100 | bad => |
110 case get_input thread_name of |
101 (Output.system_message |
111 ["continue"] => () |
102 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); |
112 | ["eval", index, language, context, expression] => |
103 debugger_loop thread_name)); |
113 (error_wrapper (fn () => |
|
114 eval (try Markup.parse_int index) (language = "SML") context expression); loop ()) |
|
115 | bad => |
|
116 (Output.system_message |
|
117 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); |
|
118 loop ())); |
|
119 in with_debugging loop; debugger_state thread_name end; |
104 |
120 |
105 fun debugger cond = |
121 fun debugger cond = |
106 if debugging () orelse not (cond ()) orelse |
122 if is_debugging () orelse not (cond ()) orelse |
107 not (Options.default_bool @{system_option ML_debugger_active}) |
123 not (Options.default_bool @{system_option ML_debugger_active}) |
108 then () |
124 then () |
109 else |
125 else |
110 with_debugging (fn () => |
126 (case Simple_Thread.get_name () of |
111 (case Simple_Thread.get_name () of |
127 NONE => () |
112 NONE => () |
128 | SOME thread_name => debugger_loop thread_name); |
113 | SOME thread_name => debugger_loop thread_name)); |
|
114 |
129 |
115 fun init () = |
130 fun init () = |
116 ML_Debugger.on_breakpoint |
131 ML_Debugger.on_breakpoint |
117 (SOME (fn (_, b) => |
132 (SOME (fn (_, b) => |
118 debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping}))); |
133 debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping}))); |