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) |