src/Pure/General/ssh.scala
changeset 80220 928e02d0cab7
parent 80218 875968a3b2f9
child 80221 0d89f0a39854
equal deleted inserted replaced
80219:840ca997deac 80220:928e02d0cab7
   337       Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out)
   337       Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out)
   338 
   338 
   339     override def tmp_file(name: String, ext: String = ""): Path = {
   339     override def tmp_file(name: String, ext: String = ""): Path = {
   340       val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext)
   340       val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext)
   341       Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out)
   341       Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out)
       
   342     }
       
   343 
       
   344     override def tmp_files(names: List[String]): List[Path] = {
       
   345       val script = names.map(name => "mktemp /tmp/" + Bash.string(name) + "-XXXXXXXXXXXX")
       
   346       Library.trim_split_lines(execute(script.mkString(" && ")).check.out).map(Path.explode)
   342     }
   347     }
   343 
   348 
   344     override def with_tmp_dir[A](body: Path => A): A = {
   349     override def with_tmp_dir[A](body: Path => A): A = {
   345       val path = tmp_dir()
   350       val path = tmp_dir()
   346       try { body(path) } finally { rm_tree(path) }
   351       try { body(path) } finally { rm_tree(path) }
   511     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
   516     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
   512     def tmp_file(name: String, ext: String = ""): Path =
   517     def tmp_file(name: String, ext: String = ""): Path =
   513       File.path(Isabelle_System.tmp_file(name, ext = ext))
   518       File.path(Isabelle_System.tmp_file(name, ext = ext))
   514     def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
   519     def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
   515       Isabelle_System.with_tmp_file(name, ext = ext)(body)
   520       Isabelle_System.with_tmp_file(name, ext = ext)(body)
       
   521     def tmp_files(names: List[String]): List[Path] = names.map(tmp_file(_))
   516     def read_dir(path: Path): List[String] = File.read_dir(path)
   522     def read_dir(path: Path): List[String] = File.read_dir(path)
   517     def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
   523     def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
   518     def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
   524     def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
   519     def read_bytes(path: Path): Bytes = Bytes.read(path)
   525     def read_bytes(path: Path): Bytes = Bytes.read(path)
   520     def read(path: Path): String = File.read(path)
   526     def read(path: Path): String = File.read(path)