support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;

--- a/src/Pure/ML/ml_system.ML	Sun Feb 07 15:32:57 2021 +0100
+++ b/src/Pure/ML/ml_system.ML	Sun Feb 07 16:31:43 2021 +0100
@@ -11,6 +11,7 @@
   val platform_is_windows: bool
   val platform_is_64: bool
   val platform_is_arm: bool
+  val platform_is_rosetta: unit -> bool
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -24,6 +25,12 @@
 val platform_is_64 = String.isPrefix "x86_64-" platform;
 val platform_is_arm = String.isPrefix "arm64-" platform;
 
+fun platform_is_rosetta () =
+  (case OS.Process.getEnv "ISABELLE_APPLE_PLATFORM64" of
+    NONE => false
+  | SOME "" => false
+  | SOME apple_platform => apple_platform <> platform);
+
 val platform_path =
   if platform_is_windows then
     fn path =>

--- a/src/Pure/System/bash.ML	Sun Feb 07 15:32:57 2021 +0100
+++ b/src/Pure/System/bash.ML	Sun Feb 07 16:31:43 2021 +0100
@@ -115,7 +115,7 @@
 val string = Bash_Syntax.string;
 val strings = Bash_Syntax.strings;
 
-val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
+val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -183,5 +183,24 @@
     handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   end);
 
+fun process_scala script =
+  Scala.function "bash_process" script
+  |> YXML.parse_body
+  |>
+    let open XML.Decode in
+      variant
+       [fn ([], []) => raise Exn.Interrupt,
+        fn ([a], []) => error a,
+        fn ([a, b], c) =>
+          let
+            val rc = int_atom a;
+            val pid = int_atom b;
+            val (out, err) = pair string string c;
+          in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end]
+    end;
+
+fun process script =
+  if ML_System.platform_is_rosetta () then process_scala script else process_ml script;
+
 end;
 \<close>
\ No newline at end of file

--- a/src/Pure/System/bash.scala	Sun Feb 07 15:32:57 2021 +0100
+++ b/src/Pure/System/bash.scala	Sun Feb 07 16:31:43 2021 +0100
@@ -202,4 +202,41 @@
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
+
+
+  /* Scala function */
+
+  object Process extends Scala.Fun("bash_process")
+  {
+    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 is_interrupt =
+        result match {
+          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)]] =
+      {
+        import XML.Encode._
+        val string = XML.Encode.string
+        variant(List(
+          { case _ if is_interrupt => (Nil, Nil) },
+          { case Exn.Exn(exn) => (List(Exn.message(exn)), Nil) },
+          { case Exn.Res((res, pid)) =>
+              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)) }))
+      }
+      YXML.string_of_body(encode(result))
+    }
+  }
 }

--- a/src/Pure/System/scala.scala	Sun Feb 07 15:32:57 2021 +0100
+++ b/src/Pure/System/scala.scala	Sun Feb 07 16:31:43 2021 +0100
@@ -243,5 +243,6 @@
   Scala.Sleep,
   Scala.Toplevel,
   Doc.Doc_Names,
+  Bash.Process,
   Bibtex.Check_Database,
   Isabelle_Tool.Isabelle_Tools)