equal
deleted
inserted
replaced
20 fun status_fn x = ! Private_Output.status_fn x; |
20 fun status_fn x = ! Private_Output.status_fn x; |
21 fun report_fn x = ! Private_Output.report_fn x; |
21 fun report_fn x = ! Private_Output.report_fn x; |
22 fun result_fn x y = ! Private_Output.result_fn x y; |
22 fun result_fn x y = ! Private_Output.result_fn x y; |
23 fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y; |
23 fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y; |
24 |
24 |
|
25 val markup_fn = Markup.output; |
|
26 |
25 end; |
27 end; |