# HG changeset patch # User wenzelm # Date 1717163801 -7200 # Node ID e0606fb415d2e58b75a72fc6cc58b5e6027602b6 # Parent 3a88980070383787fd655a597e2700f24777a9ce more operations; diff -r 3a8898007038 -r e0606fb415d2 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Fri May 31 15:38:28 2024 +0200 +++ b/src/Pure/General/ssh.scala Fri May 31 15:56:41 2024 +0200 @@ -321,7 +321,7 @@ put_file(path, File.write(_, text)) - /* tmp dirs */ + /* tmp dirs and files */ override def rm_tree(dir: Path): Unit = execute("rm -r -f " + bash_path(dir)).check @@ -329,11 +329,21 @@ override def tmp_dir(): Path = Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out) + override def tmp_file(name: String, ext: String = ""): Path = { + val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext) + Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out) + } + override def with_tmp_dir[A](body: Path => A): A = { val path = tmp_dir() try { body(path) } finally { rm_tree(path) } } + override def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { + val path = tmp_file(name, ext = ext) + try { body(path) } finally { delete(path) } + } + /* open server on remote host */ @@ -492,6 +502,10 @@ 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 tmp_file(name: String, ext: String = ""): Path = + File.path(Isabelle_System.tmp_file(name, ext = ext)) + def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = + Isabelle_System.with_tmp_file(name, ext = ext)(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) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)