# 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() }