equal
deleted
inserted
replaced
81 def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
81 def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
82 |
82 |
83 |
83 |
84 /* misc */ |
84 /* misc */ |
85 |
85 |
86 def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
86 def tmp_file(prefix: String): JFile = |
87 { |
87 { |
88 val file = JFile.createTempFile(prefix, null) |
88 val file = JFile.createTempFile(prefix, null) |
89 file.deleteOnExit |
89 file.deleteOnExit |
|
90 file |
|
91 } |
|
92 |
|
93 def with_tmp_file[A](prefix: String)(body: JFile => A): A = |
|
94 { |
|
95 val file = tmp_file(prefix) |
90 try { body(file) } finally { file.delete } |
96 try { body(file) } finally { file.delete } |
91 } |
97 } |
92 |
98 |
93 // FIXME handle (potentially cyclic) directory graph |
99 // FIXME handle (potentially cyclic) directory graph |
94 def find_files(start: JFile, ok: JFile => Boolean): List[JFile] = |
100 def find_files(start: JFile, ok: JFile => Boolean): List[JFile] = |