Pure/General/file.scala

28   /* standard path (Cygwin or Posix) */
30   def standard_path(path: Path): String = path.expand.implode
43         case path => path.replace('\\', '/')
60   /* platform path (Windows or Posix) */
78           case path if path.startsWith("/") =>
80             path
81           case path => path
93   def platform_path(path: Path): String = platform_path(standard_path(path))
94   def platform_file(path: Path): JFile = new JFile(platform_path(path))
105   def path(file: JFile): Path = Path.explode(standard_path(file))
106   def pwd(): Path = path(Path.current.absolute_file)
116       Some(path(base_path.relativize(other_path).toFile))
124   /* bash path */
126   def bash_path(path: Path): String = Bash.string(standard_path(path))
132   def check_dir(path: Path): Path =
133     if (path.is_dir) path else error("No such directory: " + path)
135   def check_file(path: Path): Path =
136     if (path.is_file) path else error("No such file: " + path)
161           override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
163             if (include_dirs) check(path.toFile)
166           override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
168             check(path.toFile)
182   def read(path: Path): String = read(path.file)
199   def read_gzip(path: Path): String = read_gzip(path.file)
203   def read_xz(path: Path): String = read_xz(path.file)
231   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
235   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
240   def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
241     write_xz(path.file, text, options)
242   def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
244   def write_backup(path: Path, text: CharSequence)
246     if (path.is_file) move(path, path.backup)
247     write(path, text)
250   def write_backup2(path: Path, text: CharSequence)
252     if (path.is_file) move(path, path.backup2)
253     write(path, text)
263   def append(path: Path, text: CharSequence): Unit = append(path.file, text)