equal
deleted
inserted
replaced
106 Output.Private_Hooks.report_fn := standard_message mbox false "C"; |
106 Output.Private_Hooks.report_fn := standard_message mbox false "C"; |
107 Output.Private_Hooks.writeln_fn := standard_message mbox true "D"; |
107 Output.Private_Hooks.writeln_fn := standard_message mbox true "D"; |
108 Output.Private_Hooks.tracing_fn := standard_message mbox true "E"; |
108 Output.Private_Hooks.tracing_fn := standard_message mbox true "E"; |
109 Output.Private_Hooks.warning_fn := standard_message mbox true "F"; |
109 Output.Private_Hooks.warning_fn := standard_message mbox true "F"; |
110 Output.Private_Hooks.error_fn := standard_message mbox true "G"; |
110 Output.Private_Hooks.error_fn := standard_message mbox true "G"; |
|
111 Output.Private_Hooks.raw_message_fn := message mbox "H"; |
111 Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; |
112 Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; |
112 Output.Private_Hooks.prompt_fn := ignore; |
113 Output.Private_Hooks.prompt_fn := ignore; |
113 message mbox "A" [] (Session.welcome ()); |
114 message mbox "A" [] (Session.welcome ()); |
114 in_stream |
115 in_stream |
115 end; |
116 end; |