equal
deleted
inserted
replaced
217 result match { |
217 result match { |
218 case Exn.Res(res) => res.rc == Exn.Interrupt.return_code |
218 case Exn.Res(res) => res.rc == Exn.Interrupt.return_code |
219 case Exn.Exn(exn) => Exn.is_interrupt(exn) |
219 case Exn.Exn(exn) => Exn.is_interrupt(exn) |
220 } |
220 } |
221 |
221 |
222 val encode: XML.Encode.T[Exn.Result[Process_Result]] = |
222 result match { |
223 { |
223 case _ if is_interrupt => "" |
224 import XML.Encode._ |
224 case Exn.Exn(exn) => Exn.message(exn) |
225 val string = XML.Encode.string |
225 case Exn.Res(res) => |
226 variant(List( |
226 (res.rc.toString :: res.out_lines.length.toString :: |
227 { case _ if is_interrupt => (Nil, Nil) }, |
227 res.out_lines ::: res.err_lines).mkString("\u0000") |
228 { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) }, |
|
229 { case Exn.Res(res) => |
|
230 val out = if (res.out_lines.isEmpty) "" else Library.terminate_lines(res.out_lines) |
|
231 val err = if (res.err_lines.isEmpty) "" else Library.terminate_lines(res.err_lines) |
|
232 (List(int_atom(res.rc)), pair(string, string)(out, err)) })) |
|
233 } |
228 } |
234 YXML.string_of_body(encode(result)) |
|
235 } |
229 } |
236 } |
230 } |
237 } |
231 } |