src/Pure/System/bash.scala

--- a/src/Pure/System/bash.scala	Sat Feb 20 21:38:23 2021 +0100
+++ b/src/Pure/System/bash.scala	Sat Feb 20 22:09:16 2021 +0100
@@ -211,30 +211,25 @@
     val here = Scala_Project.here
     def apply(script: String): String =
     {
-      val result =
-        Exn.capture {
-          val proc = process(script)
-          val res = proc.result()
-          (res, proc.pid)
-        }
+      val result = Exn.capture { Isabelle_System.bash(script) }
 
       val is_interrupt =
         result match {
-          case Exn.Res((res, _)) => res.rc == Exn.Interrupt.return_code
+          case Exn.Res(res) => res.rc == Exn.Interrupt.return_code
           case Exn.Exn(exn) => Exn.is_interrupt(exn)
         }
 
-      val encode: XML.Encode.T[Exn.Result[(Process_Result, String)]] =
+      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, pid)) =>
+          { case Exn.Res(res) =>
               val out = Library.terminate_lines(res.out_lines)
               val err = Library.terminate_lines(res.err_lines)
-              (List(int_atom(res.rc), pid), pair(string, string)(out, err)) }))
+              (List(int_atom(res.rc)), pair(string, string)(out, err)) }))
       }
       YXML.string_of_body(encode(result))
     }