more direct invocation of ML_process from Isabelle/ML via Isabelle/Scala: avoid another bulky Java process;

--- a/src/Pure/ML/ml_process.scala	Fri Nov 07 16:43:04 2025 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Nov 07 16:55:23 2025 +0100
@@ -130,16 +130,14 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)",
-    Scala_Project.here,
-    { args =>
-      var dirs: List[Path] = Nil
-      var eval_args: List[String] = Nil
-      var logic = Isabelle_System.default_logic()
-      var modes: List[String] = Nil
-      var options = Options.init()
+  def tool_body(args: List[String], internal: Boolean = false): Process_Result = {
+    var dirs: List[Path] = Nil
+    var eval_args: List[String] = Nil
+    var logic = Isabelle_System.default_logic()
+    var modes: List[String] = Nil
+    var options = Options.init()
 
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle process [OPTIONS]
 
   Options are:
@@ -152,25 +150,32 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
-        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
-        "l:" -> (arg => logic = arg),
-        "m:" -> (arg => modes = arg :: modes),
-        "o:" -> (arg => options = options + arg))
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+      "l:" -> (arg => logic = arg),
+      "m:" -> (arg => modes = arg :: modes),
+      "o:" -> (arg => options = options + arg))
 
-      val more_args = getopts(args)
-      if (args.isEmpty || more_args.nonEmpty) getopts.usage()
+    val more_args = getopts(args, internal = internal)
+    if (args.isEmpty || more_args.nonEmpty) getopts.usage(internal = internal)
 
-      val store = Store(options)
-      val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
-      val session_heaps = store.session_heaps(session_background, logic = logic)
-      val result =
-        ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes)
-          .result(
-            progress_stdout = Output.writeln(_, stdout = true),
-            progress_stderr = Output.writeln(_))
+    val store = Store(options)
+    val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
+    val session_heaps = store.session_heaps(session_background, logic = logic)
+    ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes)
+      .result(
+        progress_stdout = Output.writeln(_, stdout = true),
+        progress_stderr = Output.writeln(_))
+  }
 
-      sys.exit(result.rc)
-    })
+  val isabelle_tool =
+    Isabelle_Tool("process", "raw ML process (batch mode)", Scala_Project.here,
+      args => sys.exit(tool_body(args).rc))
+
+  object Scala_Fun extends Scala.Fun_Strings("ML_process", thread = true) {
+    val here = Scala_Project.here
+    def apply(args: List[String]): List[String] =
+      Bash.Server.result(tool_body(args, internal = true))
+  }
 }

--- a/src/Pure/System/bash.scala	Fri Nov 07 16:43:04 2025 +0100
+++ b/src/Pure/System/bash.scala	Fri Nov 07 16:55:23 2025 +0100
@@ -321,6 +321,14 @@
       server.start()
       server
     }
+
+    def result(result: Process_Result): List[String] =
+      result.rc.toString ::
+      result.timing.elapsed.ms.toString ::
+      result.timing.cpu.ms.toString ::
+      result.out_lines.length.toString ::
+      result.out_lines :::
+      result.err_lines
   }
 
   class Server private(port: Int, debugging: => Boolean)
@@ -345,14 +353,7 @@
           else List(Server.FAILURE, Exn.message(exn)))
 
       def reply_result(result: Process_Result): Unit =
-        reply(
-          Server.RESULT ::
-          result.rc.toString ::
-          result.timing.elapsed.ms.toString ::
-          result.timing.cpu.ms.toString ::
-          result.out_lines.length.toString ::
-          result.out_lines :::
-          result.err_lines)
+        reply(Server.RESULT :: Server.result(result))
 
       connection.read_byte_message().map(_.map(_.text)) match {
         case None =>

--- a/src/Pure/System/isabelle_system.ML	Fri Nov 07 16:43:04 2025 +0100
+++ b/src/Pure/System/isabelle_system.ML	Fri Nov 07 16:55:23 2025 +0100
@@ -6,6 +6,7 @@
 
 signature ISABELLE_SYSTEM =
 sig
+  val ML_process: string list -> Process_Result.T
   val bash_process: Bash.params -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
@@ -36,6 +37,32 @@
 
 val absolute_path = Path.implode o File.absolute_path;
 
+local
+
+fun bash_process_result args =
+  (case args of
+    a :: b :: c :: d :: lines =>
+      let
+        val rc = Value.parse_int a;
+        val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
+        val (out_lines, err_lines) = chop (Value.parse_int d) lines;
+      in
+        if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed
+        else
+          Process_Result.make
+           {rc = rc,
+            out_lines = out_lines,
+            err_lines = err_lines,
+            timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
+       end
+  | _ => raise Fail ("Bad number of process results " ^ string_of_int (length args)));
+
+in
+
+fun ML_process args =
+  Scala.function "ML_process" ("-o" :: ("ML_platform=" ^ ML_System.platform) :: args)
+  |> bash_process_result;
+
 fun bash_process params =
   let
     val {script, input, cwd, putenv, redirect, timeout, description} =
@@ -74,21 +101,8 @@
               else if head = Bash.server_failure andalso length args = 1 then
                 raise Fail (hd args)
               else if head = Bash.server_result andalso length args >= 4 then
-                let
-                  val a :: b :: c :: d :: lines = args;
-                  val rc = Value.parse_int a;
-                  val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
-                  val (out_lines, err_lines) = chop (Value.parse_int d) lines;
-                in
-                  if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed
-                  else
-                    Process_Result.make
-                     {rc = rc,
-                      out_lines = out_lines,
-                      err_lines = err_lines,
-                      timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
-                 end
-               else err ()
+                bash_process_result args
+              else err ()
           | _ => err ())
         and loop maybe_uuid s =
           (case Exn.capture_body (fn () => loop_body s) of
@@ -99,6 +113,8 @@
       end)
   end;
 
+end;
+
 val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
 
 fun bash_output s =

--- a/src/Pure/System/scala.scala	Fri Nov 07 16:43:04 2025 +0100
+++ b/src/Pure/System/scala.scala	Fri Nov 07 16:55:23 2025 +0100
@@ -377,5 +377,6 @@
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems,
   isabelle.atp.SystemOnTPTP.Run_System,
+  ML_Process.Scala_Fun,
   Prismjs.Languages,
   Prismjs.Tokenize)