equal
deleted
inserted
replaced
17 (* messages *) |
17 (* messages *) |
18 |
18 |
19 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
19 val _ = Session.protocol_handler "isabelle.Debugger$Handler"; |
20 |
20 |
21 fun output_message kind msg = |
21 fun output_message kind msg = |
22 Output.protocol_message |
22 if msg = "" then () |
23 (Markup.debugger_output (Simple_Thread.the_name ())) |
23 else |
24 [Markup.markup (kind, Markup.serial_properties (serial ())) msg]; |
24 Output.protocol_message |
|
25 (Markup.debugger_output (Simple_Thread.the_name ())) |
|
26 [Markup.markup (kind, Markup.serial_properties (serial ())) msg]; |
25 |
27 |
26 val writeln_message = output_message Markup.writelnN; |
28 val writeln_message = output_message Markup.writelnN; |
27 val warning_message = output_message Markup.warningN; |
29 val warning_message = output_message Markup.warningN; |
28 val error_message = output_message Markup.errorN; |
30 val error_message = output_message Markup.errorN; |
29 |
31 |