src/Pure/System/bash.scala

--- a/src/Pure/System/bash.scala	Sun Feb 21 12:24:40 2021 +0100
+++ b/src/Pure/System/bash.scala	Sun Feb 21 13:14:08 2021 +0100
@@ -219,19 +219,13 @@
           case Exn.Exn(exn) => Exn.is_interrupt(exn)
         }
 
-      val encode: XML.Encode.T[Exn.Result[Process_Result]] =
-      {
-        import XML.Encode._
-        val string = XML.Encode.string
-        variant(List(
-          { case _ if is_interrupt => (Nil, Nil) },
-          { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
-          { case Exn.Res(res) =>
-              val out = if (res.out_lines.isEmpty) "" else Library.terminate_lines(res.out_lines)
-              val err = if (res.err_lines.isEmpty) "" else Library.terminate_lines(res.err_lines)
-              (List(int_atom(res.rc)), pair(string, string)(out, err)) }))
+      result match {
+        case _ if is_interrupt => ""
+        case Exn.Exn(exn) => Exn.message(exn)
+        case Exn.Res(res) =>
+          (res.rc.toString :: res.out_lines.length.toString ::
+            res.out_lines ::: res.err_lines).mkString("\u0000")
       }
-      YXML.string_of_body(encode(result))
     }
   }
 }