# HG changeset patch
# User wenzelm
# Date 1674654673 -3600
# Node ID 4d9f3d1e1749530a72d282ea4cb58e8571f33fcc
# Parent  15e710116a169b09d424fe5df5d276270057d1f1
more operations for SSH.System;

diff -r 15e710116a16 -r 4d9f3d1e1749 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Jan 25 13:38:26 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Jan 25 14:51:13 2023 +0100
@@ -583,7 +583,7 @@
         yield {
           val log = Path.explode(line)
           val bytes = ssh.read_bytes(log)
-          ssh.rm(log)
+          ssh.delete(log)
           (log.file_name, bytes)
         }
       }
diff -r 15e710116a16 -r 4d9f3d1e1749 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Jan 25 13:38:26 2023 +0100
+++ b/src/Pure/General/ssh.scala	Wed Jan 25 14:51:13 2023 +0100
@@ -120,6 +120,7 @@
       opts: String = "",
       args: String = "",
       cwd: JFile = null,
+      redirect: Boolean = false,
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
       strict: Boolean = true
@@ -131,8 +132,11 @@
         Config.command(command, config) +
         (if (opts.nonEmpty) " " + opts else "") +
         (if (args.nonEmpty) " -- " + args else "")
-      Isabelle_System.bash(cmd, cwd = cwd, progress_stdout = progress_stdout,
-        progress_stderr = progress_stderr, strict = strict)
+      Isabelle_System.bash(cmd, cwd = cwd,
+        redirect = redirect,
+        progress_stdout = progress_stdout,
+        progress_stderr = progress_stderr,
+        strict = strict)
     }
 
     def run_sftp(
@@ -183,6 +187,7 @@
     override def execute(cmd_line: String,
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
+      redirect: Boolean = false,
       settings: Boolean = true,
       strict: Boolean = true
     ): Process_Result = {
@@ -190,6 +195,7 @@
         args = Bash.string(host) + " " + Bash.string(cmd_line),
         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
+        redirect = redirect,
         strict = strict)
     }
 
@@ -222,11 +228,19 @@
     override def bash_path(path: Path): String = Bash.string(remote_path(path))
     def sftp_path(path: Path): String = sftp_string(remote_path(path))
 
-    def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path))
-
     override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
     override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).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 set_executable(path: Path, flag: Boolean): Unit =
+      if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
+        error("Failed to change executable status of " + quote(remote_path(path)))
+      }
+
     override def make_directory(path: Path): Path = {
       if (!execute("mkdir -p " + bash_path(path)).ok) {
         error("Failed to create directory: " + quote(remote_path(path)))
@@ -267,15 +281,15 @@
 
     override def write_file(path: Path, local_path: Path): Unit =
       put_file(path, Isabelle_System.copy_file(local_path, _))
-    def write_bytes(path: Path, bytes: Bytes): Unit =
+    override def write_bytes(path: Path, bytes: Bytes): Unit =
       put_file(path, Bytes.write(_, bytes))
-    def write(path: Path, text: String): Unit =
+    override def write(path: Path, text: String): Unit =
       put_file(path, File.write(_, text))
 
 
     /* tmp dirs */
 
-    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
+    override def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
 
     def rm_tree(remote_dir: String): Unit =
       execute("rm -r -f " + Bash.string(remote_dir)).check
@@ -367,22 +381,29 @@
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
+    def delete(path: Path): Unit = path.file.delete
+    def set_executable(path: Path, flag: Boolean): Unit = File.set_executable(path, flag)
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
+    def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
     def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
     def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
-    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
     def read_bytes(path: Path): Bytes = Bytes.read(path)
     def read(path: Path): String = File.read(path)
+    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
+    def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes)
+    def write(path: Path, text: String): Unit = File.write(path, text)
 
     def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
+        redirect: Boolean = false,
         settings: Boolean = true,
         strict: Boolean = true): Process_Result =
       Isabelle_System.bash(command,
         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
+        redirect = redirect,
         env = if (settings) Isabelle_System.settings() else null,
         strict = strict)