# HG changeset patch
# User wenzelm
# Date 1612726755 -3600
# Node ID d1bc5a376cf91e43141e7dcce41720ab8a0a89bc
# Parent  5be512af2a86d755638e219c4ad3f8236ebeb130
more robust: allow YXML text;

diff -r 5be512af2a86 -r d1bc5a376cf9 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Sun Feb 07 17:00:03 2021 +0100
+++ b/src/Pure/System/bash.ML	Sun Feb 07 20:39:15 2021 +0100
@@ -191,12 +191,12 @@
     let open XML.Decode in
       variant
        [fn ([], []) => raise Exn.Interrupt,
-        fn ([a], []) => error a,
+        fn ([], a) => error (YXML.string_of_body a),
         fn ([a, b], c) =>
           let
             val rc = int_atom a;
             val pid = int_atom b;
-            val (out, err) = pair string string c;
+            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
           in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end]
     end;
 
diff -r 5be512af2a86 -r d1bc5a376cf9 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun Feb 07 17:00:03 2021 +0100
+++ b/src/Pure/System/bash.scala	Sun Feb 07 20:39:15 2021 +0100
@@ -230,7 +230,7 @@
         val string = XML.Encode.string
         variant(List(
           { case _ if is_interrupt => (Nil, Nil) },
-          { case Exn.Exn(exn) => (List(Exn.message(exn)), Nil) },
+          { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
           { case Exn.Res((res, pid)) =>
               val out = Library.terminate_lines(res.out_lines)
               val err = Library.terminate_lines(res.err_lines)