src/Pure/System/bash.scala
changeset 73268 c8abfe393c16
parent 73265 76c9fcf80f96
child 73273 17c28251fff0
equal deleted inserted replaced
73267:1d610d5524ff 73268:c8abfe393c16
   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 }