# HG changeset patch
# User wenzelm
# Date 1717161977 -7200
# Node ID c6d18c836509ab1ca9e58bb189a371279fafcaab
# Parent  d78446e2b6130a9b9d6aa3bf818037aba2e47b86
clarified signature;

diff -r d78446e2b613 -r c6d18c836509 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri May 31 14:17:28 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 31 15:26:17 2024 +0200
@@ -323,18 +323,16 @@
 
     /* tmp dirs */
 
-    override def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
+    override def rm_tree(dir: Path): Unit =
+      execute("rm -r -f " + bash_path(dir)).check
 
-    def rm_tree(remote_dir: String): Unit =
-      execute("rm -r -f " + Bash.string(remote_dir)).check
-
-    def tmp_dir(): String =
-      execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out
+    override def tmp_dir(): Path =
+      Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out)
 
     override def with_tmp_dir[A](body: Path => A): A = {
-      val remote_dir = tmp_dir()
-      try { body(Path.explode(remote_dir)) }
-      finally { rm_tree(remote_dir) }
+      val dir = tmp_dir()
+      try { body(dir) }
+      finally { rm_tree(dir) }
     }
 
 
@@ -493,6 +491,7 @@
       File.set_executable(path, reset = reset)
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
     def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
+    def tmp_dir(): Path = File.path(Isabelle_System.tmp_dir("tmp"))
     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
     def read_dir(path: Path): List[String] = File.read_dir(path)
     def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)