Pure/General/file.scala

1 /*  Title:      Pure/General/file.scala
13 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
15 import java.nio.file.attribute.BasicFileAttributes
49   def standard_path(file: JFile): String = standard_path(file.getPath)
54       if (url.getProtocol == "file" && Url.is_wellformed_file(name))
100   def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
101   def absolute_name(file: JFile): String = absolute(file).getPath
103   def canonical(file: JFile): JFile = file.getCanonicalFile
104   def canonical_name(file: JFile): String = canonical(file).getPath
106   def path(file: JFile): Path = Path.explode(standard_path(file))
114     val base_path = base.file.toPath
115     val other_path = other.file.toPath
125   def bash_path(file: JFile): String = Bash.string(standard_path(file))
134     if (path.is_file) path else error("No such file: " + path)
142     val files = dir.file.listFiles
154     def check(file: JFile) { if (pred(file)) result += file }
170             val file = path.toFile
171             if (include_dirs || !file.isDirectory) check(file)
184   def read(file: JFile): String = Bytes.read(file).text
185   def read(path: Path): String = read(path.file)
200   def read_gzip(file: JFile): String =
201     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
202   def read_gzip(path: Path): String = read_gzip(path.file)
204   def read_xz(file: JFile): String =
205     read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
206   def read_xz(path: Path): String = read_xz(path.file)
234   def writer(file: JFile): BufferedWriter =
235     new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
237   def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
239     val stream = make_stream(new FileOutputStream(file))
243   def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
244   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
246   def write_gzip(file: JFile, text: CharSequence): Unit =
247     write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
248   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
250   def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
251     File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
252   def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
254     write_xz(path.file, text, options)
272   def append(file: JFile, text: CharSequence): Unit =
273     Files.write(file.toPath, UTF8.bytes(text.toString),
276   def append(path: Path, text: CharSequence): Unit = append(path.file, text)
282     try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
285   def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
295   def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
309   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
321   def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
328     val src_file = src.file
329     val dst_file = dst.file
349     else path.file.canExecute
356     else path.file.setExecutable(flag, false)