more robust: allow YXML text;
authorwenzelm
Sun, 07 Feb 2021 20:39:15 +0100
changeset 73230 d1bc5a376cf9
parent 73229 5be512af2a86
child 73231 0659fc0ed877
more robust: allow YXML text;
src/Pure/System/bash.ML
src/Pure/System/bash.scala
--- 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;
 
--- 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)