more SSH operations;

--- a/src/Pure/General/ssh.scala	Thu Mar 30 12:56:29 2023 +0200
+++ b/src/Pure/General/ssh.scala	Thu Mar 30 14:25:31 2023 +0200
@@ -408,6 +408,10 @@
         env = if (settings) Isabelle_System.settings() else null,
         strict = strict)
 
+    def new_directory(path: Path): Path =
+      if (is_dir(path)) error("Directory already exists: " + absolute_path(path))
+      else make_directory(path)
+
     def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
       Isabelle_System.download_file(url_name, file, progress = progress)
 

--- a/src/Pure/System/components.scala	Thu Mar 30 12:56:29 2023 +0200
+++ b/src/Pure/System/components.scala	Thu Mar 30 14:25:31 2023 +0200
@@ -171,10 +171,11 @@
   /* component directory content */
 
   object Directory {
-    def apply(path: Path): Directory = new Directory(path.absolute)
+    def apply(path: Path, ssh: SSH.System = SSH.Local): Directory =
+      new Directory(ssh.absolute_path(path), ssh)
   }
 
-  class Directory private(val path: Path) {
+  class Directory private(val path: Path, val ssh: SSH.System = SSH.Local) {
     override def toString: String = path.toString
 
     def etc: Path = path + Path.basic("etc")
@@ -188,15 +189,16 @@
 
     def create(progress: Progress = new Progress): Directory = {
       progress.echo("Creating component directory " + path)
-      Isabelle_System.new_directory(path)
-      Isabelle_System.make_directory(etc)
+      ssh.new_directory(path)
+      ssh.make_directory(etc)
       this
     }
 
-    def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path)
+    def ok: Boolean =
+      ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh)
 
     def check: Directory =
-      if (!path.is_dir) error("Bad component directory: " + path)
+      if (!ssh.is_dir(path)) error("Bad component directory: " + path)
       else if (!ok) {
         error("Malformed component directory: " + path +
           "\n  (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
@@ -204,12 +206,12 @@
       else this
 
     def read_components(): List[String] =
-      split_lines(File.read(components)).filter(_.nonEmpty)
+      split_lines(ssh.read(components)).filter(_.nonEmpty)
     def write_components(lines: List[String]): Unit =
-      File.write(components, terminate_lines(lines))
+      ssh.write(components, terminate_lines(lines))
 
     def write_settings(text: String): Unit =
-      File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
+      ssh.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
   }
 
 

--- a/src/Pure/Thy/sessions.scala	Thu Mar 30 12:56:29 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 30 14:25:31 2023 +0200
@@ -1255,8 +1255,8 @@
 
   /* load sessions from certain directories */
 
-  def is_session_dir(dir: Path): Boolean =
-    (dir + ROOT).is_file || (dir + ROOTS).is_file
+  def is_session_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean =
+    ssh.is_file(dir + ROOT) || ssh.is_file(dir + ROOTS)
 
   def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
@@ -1266,7 +1266,7 @@
     }
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
-    val default_dirs = Components.directories().filter(is_session_dir)
+    val default_dirs = Components.directories().filter(is_session_dir(_))
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }