# HG changeset patch
# User wenzelm
# Date 1738752951 -3600
# Node ID 794bf73e100f31ee5aec2d9c81b08c11339d1af7
# Parent  2028082805f00f094779e359be48d5427a5dc54a
clarified signature: scalable Bash.input thanks to Bytes.T;

diff -r 2028082805f0 -r 794bf73e100f src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Tue Feb 04 22:21:36 2025 +0100
+++ b/src/Pure/System/bash.ML	Wed Feb 05 11:55:51 2025 +0100
@@ -10,10 +10,10 @@
   val strings: string list -> string
   type params
   val dest_params: params ->
-   {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+   {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
     redirect: bool, timeout: Time.time, description: string}
   val script: string -> params
-  val input: string -> params -> params
+  val input: Bytes.T -> params -> params
   val cwd: Path.T -> params -> params
   val putenv: (string * string) list -> params -> params
   val redirect: params -> params
@@ -56,7 +56,7 @@
 
 abstype params =
   Params of
-   {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+   {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
     redirect: bool, timeout: Time.time, description: string}
 with
 
@@ -69,7 +69,7 @@
 fun map_params f (Params {script, input, cwd, putenv, redirect, timeout, description}) =
   make_params (f (script, input, cwd, putenv, redirect, timeout, description));
 
-fun script script = make_params (script, "", NONE, [], false, Time.zeroTime, "");
+fun script script = make_params (script, Bytes.empty, NONE, [], false, Time.zeroTime, "");
 
 fun input input =
   map_params (fn (script, _, cwd, putenv, redirect, timeout, description) =>
diff -r 2028082805f0 -r 794bf73e100f src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Feb 04 22:21:36 2025 +0100
+++ b/src/Pure/System/isabelle_system.ML	Wed Feb 05 11:55:51 2025 +0100
@@ -41,13 +41,15 @@
     val {script, input, cwd, putenv, redirect, timeout, description} =
       Bash.dest_params params;
     val server_run =
-      [Bash.server_run, script, input,
-        let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
-        let open XML.Encode in YXML.string_of_body o list (pair string string) end
-          (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
-        Value.print_bool redirect,
-        Value.print_real (Time.toReal timeout),
-        description];
+     [Bytes.string Bash.server_run,
+      Bytes.string script,
+      input,
+      let open XML.Encode in YXML.bytes_of_body (option (string o absolute_path) cwd) end,
+      let open XML.Encode in YXML.bytes_of_body o list (pair string string) end
+        (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
+      Bytes.string (Value.print_bool redirect),
+      Bytes.string (Value.print_real (Time.toReal timeout)),
+      Bytes.string description];
 
     val address = Options.default_string \<^system_option>\<open>bash_process_address\<close>;
     val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>;
@@ -93,7 +95,7 @@
             Exn.Res res => res
           | Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
       in
-        with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
+        with_streams (fn s => (Byte_Message.write_message (#2 s) server_run; loop NONE s))
       end)
   end;