provide local component to remote directory;

--- a/src/Pure/System/components.scala	Thu Mar 30 15:31:55 2023 +0200
+++ b/src/Pure/System/components.scala	Thu Mar 30 15:33:02 2023 +0200
@@ -64,6 +64,7 @@
 
   val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
   val dynamic_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}"
+  val classic_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib")
 
   val default_catalogs: List[String] = List("main")
   val optional_catalogs: List[String] = List("main", "optional")
@@ -157,6 +158,31 @@
     }
   }
 
+  def provide(local_dir: Path,
+    base_dir: Path = classic_components_base,
+    ssh: SSH.System = SSH.Local,
+    progress: Progress = new Progress
+  ): Directory = {
+    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) {
+      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 =>
+          val remote_tmp_tar = remote_tmp_dir + Path.basic("tmp.tar")
+          val remote_dir = ssh.make_directory(remote_directory.path)
+          Isabelle_System.gnutar(
+            "-cf " + File.bash_path(local_tmp_tar) + " .", dir = local_dir).check
+          ssh.write_file(remote_tmp_tar, local_tmp_tar)
+          ssh.execute(
+            "tar -C " + ssh.bash_path(remote_dir) + " -xf " + ssh.bash_path(remote_tmp_tar)).check
+        }
+      }
+    }
+    remote_directory.check
+  }
+
 
   /* component directories */