# HG changeset patch
# User wenzelm
# Date 1717184341 -7200
# Node ID 928e02d0cab77353d793c14b957f1ad4500d1a4e
# Parent  840ca997deac8e33124d41f9297b9c04dd646e77
minor performance tuning: save approx. 70ms per SSH command;

diff -r 840ca997deac -r 928e02d0cab7 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri May 31 21:17:01 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 31 21:39:01 2024 +0200
@@ -341,6 +341,11 @@
       Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out)
     }
 
+    override def tmp_files(names: List[String]): List[Path] = {
+      val script = names.map(name => "mktemp /tmp/" + Bash.string(name) + "-XXXXXXXXXXXX")
+      Library.trim_split_lines(execute(script.mkString(" && ")).check.out).map(Path.explode)
+    }
+
     override def with_tmp_dir[A](body: Path => A): A = {
       val path = tmp_dir()
       try { body(path) } finally { rm_tree(path) }
@@ -513,6 +518,7 @@
       File.path(Isabelle_System.tmp_file(name, ext = ext))
     def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
       Isabelle_System.with_tmp_file(name, ext = ext)(body)
+    def tmp_files(names: List[String]): List[Path] = names.map(tmp_file(_))
     def read_dir(path: Path): List[String] = File.read_dir(path)
     def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
     def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
diff -r 840ca997deac -r 928e02d0cab7 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Fri May 31 21:17:01 2024 +0200
+++ b/src/Pure/System/bash.scala	Fri May 31 21:39:01 2024 +0200
@@ -96,11 +96,12 @@
             """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n"
       }
 
-    private val timing_file = ssh.tmp_file("bash_timing")
+    private val List(timing_file, script_file) =
+      ssh.tmp_files(List("bash_timing", "bash_script"))
+
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
 
-    private val script_file: Path = ssh.tmp_file("bash_script")
     ssh.write(script_file, winpid_script + script)
 
     private val ssh_file: Option[JFile] =