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

diff -r 928e02d0cab7 -r 0d89f0a39854 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri May 31 21:39:01 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 31 22:10:11 2024 +0200
@@ -265,10 +265,14 @@
     override def eq_file(path1: Path, path2: Path): Boolean =
       path1 == path2 || execute("test " + bash_path(path1) + " -ef " + bash_path(path2)).ok
 
-    override def delete(path: Path): Unit = {
-      val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else ""
-      if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
-    }
+    override def delete(paths: Path*): Unit =
+      if (paths.nonEmpty) {
+        val script =
+          "set -e\n" +
+          "for X in " + paths.iterator.map(bash_path).mkString(" ") + "\n" +
+          """do if test -d "$X"; then rmdir "$X"; else rm -f "$X"; fi; done"""
+        execute(script).check
+      }
 
     override def restrict(path: Path): Unit =
       if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) {
@@ -506,7 +510,7 @@
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
     def eq_file(path1: Path, path2: Path): Boolean = File.eq(path1, path2)
-    def delete(path: Path): Unit = path.file.delete
+    def delete(paths: Path*): Unit = paths.foreach(path => path.file.delete)
     def restrict(path: Path): Unit = File.restrict(path)
     def set_executable(path: Path, reset: Boolean = false): Unit =
       File.set_executable(path, reset = reset)
diff -r 928e02d0cab7 -r 0d89f0a39854 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Fri May 31 21:39:01 2024 +0200
+++ b/src/Pure/System/bash.scala	Fri May 31 22:10:11 2024 +0200
@@ -192,24 +192,23 @@
       winpid_file.foreach(_.delete())
       ssh_file.foreach(_.delete())
 
-      ssh.delete(script_file)
-
       timing.change {
         case None =>
-          if (ssh.is_file(timing_file)) {
-            val t =
-              Word.explode(ssh.read(timing_file)) match {
-                case List(Value.Long(elapsed), Value.Long(cpu)) =>
-                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
-                case _ => Timing.zero
-              }
-            ssh.delete(timing_file)
-            Some(t)
-          }
-          else Some(Timing.zero)
+          val timing_text =
+            try { ssh.read(timing_file) }
+            catch { case ERROR(_) => "" }
+          val t =
+            Word.explode(timing_text) match {
+              case List(Value.Long(elapsed), Value.Long(cpu)) =>
+                Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
+              case _ => Timing.zero
+            }
+          Some(t)
         case some => some
       }
 
+      ssh.delete(timing_file, script_file)
+
       cleanup()
     }