more accurate process_result in ML, corresponding to Process_Result in 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))
     }
   }
 }

--- a/src/Pure/System/isabelle_system.ML	Sun Feb 21 12:24:40 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sun Feb 21 13:14:08 2021 +0100
@@ -6,7 +6,9 @@
 
 signature ISABELLE_SYSTEM =
 sig
-  val bash_process: string -> {out: string, err: string, rc: int}
+  type process_result =
+    {rc: int, out_lines: string list, err_lines: string list, out: string, err: string}
+  val bash_process: string -> process_result
   val bash_output_check: string -> string
   val bash_output: string -> string * int
   val bash: string -> int
@@ -29,21 +31,21 @@
 
 (* bash *)
 
-fun bash_process script =
+type process_result =
+  {rc: int, out_lines: string list, err_lines: string list, out: string, err: string};
+
+fun bash_process script : process_result =
   Scala.function_thread "bash_process"
     ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
-  |> YXML.parse_body
-  |>
-    let open XML.Decode in
-      variant
-       [fn ([], []) => raise Exn.Interrupt,
-        fn ([], a) => error (YXML.string_of_body a),
-        fn ([a], c) =>
+  |> space_explode "\000"
+  |> (fn [] => raise Exn.Interrupt
+      | [err] => error err
+      | a :: b :: lines =>
           let
-            val rc = int_atom a;
-            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
-          in {out = out, err = err, rc = rc} end]
-    end;
+            val rc = Value.parse_int a;
+            val ((out, err), (out_lines, err_lines)) =
+              chop (Value.parse_int b) lines |> `(apply2 cat_lines);
+          in {rc = rc, out_lines = out_lines, err_lines = err_lines, out = out, err = err} end);
 
 fun bash_output_check s =
   (case bash_process s of