# HG changeset patch
# User wenzelm
# Date 1717183021 -7200
# Node ID 840ca997deac8e33124d41f9297b9c04dd646e77
# Parent  875968a3b2f92acd315a61754928f873aa0e5b81
minor performance tuning: save approx. 70ms per SSH test command;

diff -r 875968a3b2f9 -r 840ca997deac src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Fri May 31 20:46:51 2024 +0200
+++ b/src/Pure/System/components.scala	Fri May 31 21:17:01 2024 +0200
@@ -153,7 +153,8 @@
     val base_name = local_dir.expand.base
     val local_directory = Directory(local_dir).check
     val remote_directory = Directory(base_dir + base_name, ssh = ssh)
-    if (!remote_directory.ok) {
+    if (remote_directory.ok) remote_directory
+    else {
       progress.echo("Providing " + base_name + ssh.print)
       Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar =>
         ssh.with_tmp_dir { remote_tmp_dir =>
@@ -166,8 +167,8 @@
             "tar -C " + ssh.bash_path(remote_dir) + " -xf " + ssh.bash_path(remote_tmp_tar)).check
         }
       }
+      remote_directory.check
     }
-    remote_directory.check
   }
 
 
@@ -253,12 +254,12 @@
       ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh)
 
     def check: Directory =
-      if (!ssh.is_dir(path)) error("Bad component directory: " + toString)
-      else if (!ok) {
+      if (ok) this
+      else if (!ssh.is_dir(path)) error("Bad component directory: " + toString)
+      else {
         error("Malformed component directory: " + toString +
           "\n  (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
       }
-      else this
 
     def read_components(): List[String] =
       split_lines(ssh.read(components)).filter(_.nonEmpty)