manage other Isabelle distributions via SSH;

--- a/src/Pure/Admin/other_isabelle.scala	Wed Jan 25 14:51:13 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Jan 25 14:58:34 2023 +0100
@@ -10,24 +10,33 @@
 
 object Other_Isabelle {
   def apply(
-    isabelle_home: Path,
+    root: Path,
     isabelle_identifier: String = "",
+    ssh: SSH.System = SSH.Local,
     progress: Progress = new Progress
   ): Other_Isabelle = {
-    if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
-      error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
-    }
-
-    new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress)
+    val (isabelle_home, url_prefix) =
+      ssh match {
+        case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix)
+        case _ =>
+          if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
+            error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT")
+          }
+          (root.canonical, "")
+      }
+    val isabelle_home_url = url_prefix + isabelle_home.implode
+    new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress)
   }
 }
 
 final class Other_Isabelle private(
   val isabelle_home: Path,
   val isabelle_identifier: String,
+  isabelle_home_url: String,
+  ssh: SSH.System,
   progress: Progress
 ) {
-  override def toString: String = isabelle_home.toString
+  override def toString: String = isabelle_home_url
 
 
   /* static system */
@@ -38,9 +47,14 @@
     echo: Boolean = false,
     strict: Boolean = true
   ): Process_Result = {
-    progress.bash(
-      Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
-      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
+    ssh.execute(
+      Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+        "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
+      progress_stdout = progress.echo_if(echo, _),
+      progress_stderr = progress.echo_if(echo, _),
+      redirect = redirect,
+      settings = false,
+      strict = strict)
   }
 
   def getenv(name: String): String =
@@ -57,27 +71,19 @@
   def etc_settings: Path = etc + Path.explode("settings")
   def etc_preferences: Path = etc + Path.explode("preferences")
 
-  def resolve_components(echo: Boolean = false): Unit = {
-    val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
-    for (path <- missing) {
-      Components.resolve(path.dir, path.file_name,
-        progress = if (echo) progress else new Progress)
-    }
-  }
-
   def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
-    if (fresh) {
-      Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
-    }
+    if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes"))
 
     val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
-    if (!expand_path(dummy_stty).is_file) {
-      Isabelle_System.copy_file(dummy_stty,
-        Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
+    val dummy_stty_remote = expand_path(dummy_stty)
+    if (!ssh.is_file(dummy_stty_remote)) {
+      ssh.make_directory(dummy_stty_remote.dir)
+      ssh.write_file(dummy_stty_remote, dummy_stty)
+      ssh.set_executable(dummy_stty_remote, true)
     }
     try {
       bash(
-        "export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
+        "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" +
         "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
         "bin/isabelle jedit -b", echo = echo).check
     }
@@ -102,21 +108,29 @@
       "init_component " + quote(components_base) + "/" + name)
   }
 
+  def resolve_components(echo: Boolean = false): Unit = {
+    val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
+    for (path <- missing) {
+      Components.resolve(path.dir, path.file_name, ssh = ssh,
+        progress = if (echo) progress else new Progress)
+    }
+  }
+
 
   /* settings */
 
   def clean_settings(): Boolean =
-    if (!etc_settings.is_file) true
-    else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
-      etc_settings.file.delete
+    if (!ssh.is_file(etc_settings)) true
+    else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) {
+      ssh.delete(etc_settings)
       true
     }
     else false
 
   def init_settings(settings: List[String]): Unit = {
     if (clean_settings()) {
-      Isabelle_System.make_directory(etc_settings.dir)
-      File.write(etc_settings,
+      ssh.make_directory(etc_settings.dir)
+      ssh.write(etc_settings,
         "# generated by Isabelle " + Date.now() + "\n" +
         "#-*- shell-script -*- :mode=shellscript:\n" +
         settings.mkString("\n", "\n", "\n"))
@@ -129,7 +143,7 @@
 
   def cleanup(): Unit = {
     clean_settings()
-    etc.file.delete
-    isabelle_home_user.file.delete
+    ssh.delete(etc)
+    ssh.delete(isabelle_home_user)
   }
 }