64 |
64 |
65 local |
65 local |
66 |
66 |
67 fun chunk s = [string_of_int (size s), "\n", s]; |
67 fun chunk s = [string_of_int (size s), "\n", s]; |
68 |
68 |
69 fun message mbox ch raw_props body = |
69 fun message do_flush mbox ch raw_props body = |
70 let |
70 let |
71 val robust_props = map (pairself YXML.embed_controls) raw_props; |
71 val robust_props = map (pairself YXML.embed_controls) raw_props; |
72 val header = YXML.string_of (XML.Elem ((ch, robust_props), [])); |
72 val header = YXML.string_of (XML.Elem ((ch, robust_props), [])); |
73 in Mailbox.send mbox (chunk header @ chunk body) end; |
73 in Mailbox.send mbox (chunk header @ chunk body, do_flush) end; |
74 |
74 |
75 fun standard_message mbox opt_serial ch body = |
75 fun standard_message mbox opt_serial ch body = |
76 if body = "" then () |
76 if body = "" then () |
77 else |
77 else |
78 message mbox ch |
78 message false mbox ch |
79 ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I) |
79 ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I) |
80 (Position.properties_of (Position.thread_data ()))) body; |
80 (Position.properties_of (Position.thread_data ()))) body; |
81 |
81 |
82 fun message_output mbox out_stream = |
82 fun message_output mbox out_stream = |
83 let |
83 let |
|
84 fun flush () = ignore (try TextIO.flushOut out_stream); |
84 fun loop receive = |
85 fun loop receive = |
85 (case receive mbox of |
86 (case receive mbox of |
86 SOME msg => |
87 SOME (msg, do_flush) => |
87 (List.app (fn s => TextIO.output (out_stream, s)) msg; |
88 (List.app (fn s => TextIO.output (out_stream, s)) msg; |
|
89 if do_flush then flush () else (); |
88 loop (Mailbox.receive_timeout (seconds 0.02))) |
90 loop (Mailbox.receive_timeout (seconds 0.02))) |
89 | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive))); |
91 | NONE => (flush (); loop (SOME o Mailbox.receive))); |
90 in fn () => loop (SOME o Mailbox.receive) end; |
92 in fn () => loop (SOME o Mailbox.receive) end; |
91 |
93 |
92 in |
94 in |
93 |
95 |
94 fun setup_channels in_fifo out_fifo = |
96 fun setup_channels in_fifo out_fifo = |
98 val out_stream = TextIO.openOut out_fifo; |
100 val out_stream = TextIO.openOut out_fifo; |
99 |
101 |
100 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); |
102 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); |
101 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); |
103 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); |
102 |
104 |
103 val mbox = Mailbox.create () : string list Mailbox.T; |
105 val mbox = Mailbox.create () : (string list * bool) Mailbox.T; |
104 val _ = Simple_Thread.fork false (message_output mbox out_stream); |
106 val _ = Simple_Thread.fork false (message_output mbox out_stream); |
105 in |
107 in |
106 Output.Private_Hooks.status_fn := standard_message mbox NONE "B"; |
108 Output.Private_Hooks.status_fn := standard_message mbox NONE "B"; |
107 Output.Private_Hooks.report_fn := standard_message mbox NONE "C"; |
109 Output.Private_Hooks.report_fn := standard_message mbox NONE "C"; |
108 Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s); |
110 Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s); |
109 Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s); |
111 Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s); |
110 Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s); |
112 Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s); |
111 Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s); |
113 Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s); |
112 Output.Private_Hooks.raw_message_fn := message mbox "H"; |
114 Output.Private_Hooks.raw_message_fn := message true mbox "H"; |
113 Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; |
115 Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; |
114 Output.Private_Hooks.prompt_fn := ignore; |
116 Output.Private_Hooks.prompt_fn := ignore; |
115 message mbox "A" [] (Session.welcome ()); |
117 message true mbox "A" [] (Session.welcome ()); |
116 in_stream |
118 in_stream |
117 end; |
119 end; |
118 |
120 |
119 end; |
121 end; |
120 |
122 |