equal
deleted
inserted
replaced
20 |
20 |
21 fun output_message kind msg = |
21 fun output_message kind msg = |
22 if msg = "" then () |
22 if msg = "" then () |
23 else |
23 else |
24 Output.protocol_message |
24 Output.protocol_message |
25 (Markup.debugger_output (Isabelle_Thread.the_name ())) |
25 (Markup.debugger_output (Isabelle_Thread.get_name ())) |
26 [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]; |
26 [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]; |
27 |
27 |
28 val writeln_message = output_message Markup.writelnN; |
28 val writeln_message = output_message Markup.writelnN; |
29 val warning_message = output_message Markup.warningN; |
29 val warning_message = output_message Markup.warningN; |
30 val error_message = output_message Markup.errorN; |
30 val error_message = output_message Markup.errorN; |
248 (init_input (); |
248 (init_input (); |
249 PolyML.DebuggerInterface.setOnBreakPoint |
249 PolyML.DebuggerInterface.setOnBreakPoint |
250 (SOME (fn (_, break) => |
250 (SOME (fn (_, break) => |
251 if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ()) |
251 if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ()) |
252 then |
252 then |
253 (case Isabelle_Thread.get_name () of |
253 (case try Isabelle_Thread.get_name () of |
254 SOME thread_name => debugger_loop thread_name |
254 SOME thread_name => debugger_loop thread_name |
255 | NONE => ()) |
255 | NONE => ()) |
256 else ())))); |
256 else ())))); |
257 |
257 |
258 val _ = |
258 val _ = |