1/* Title: Pure/General/file.scala 2 Author: Makarius 3 4File-system operations. 5*/ 6 7package isabelle 8 9 10import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, 11 OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, 12 InputStreamReader, File => JFile, IOException} 13import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath, 14 Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException} 15import java.nio.file.attribute.BasicFileAttributes 16import java.net.{URL, MalformedURLException} 17import java.util.zip.{GZIPInputStream, GZIPOutputStream} 18import java.util.regex.Pattern 19import java.util.EnumSet 20 21import org.tukaani.xz.{XZInputStream, XZOutputStream} 22 23import scala.collection.mutable 24import scala.util.matching.Regex 25 26 27object File 28{ 29 /* standard path (Cygwin or Posix) */ 30 31 def standard_path(path: Path): String = path.expand.implode 32 33 def standard_path(platform_path: String): String = 34 if (Platform.is_windows) { 35 val Platform_Root = new Regex("(?i)" + 36 Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") 37 val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") 38 39 platform_path.replace('/', '\\') match { 40 case Platform_Root(rest) => "/" + rest.replace('\\', '/') 41 case Drive(letter, rest) => 42 "/cygdrive/" + Word.lowercase(letter) + 43 (if (rest == "") "" else "/" + rest.replace('\\', '/')) 44 case path => path.replace('\\', '/') 45 } 46 } 47 else platform_path 48 49 def standard_path(file: JFile): String = standard_path(file.getPath) 50 51 def standard_url(name: String): String = 52 try { 53 val url = new URL(name) 54 if (url.getProtocol == "file" && Url.is_wellformed_file(name)) 55 standard_path(Url.parse_file(name)) 56 else name 57 } 58 catch { case _: MalformedURLException => standard_path(name) } 59 60 61 /* platform path (Windows or Posix) */ 62 63 private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") 64 private val Named_Root = new Regex("//+([^/]*)(.*)") 65 66 def platform_path(standard_path: String): String = 67 if (Platform.is_windows) { 68 val result_path = new StringBuilder 69 val rest = 70 standard_path match { 71 case Cygdrive(drive, rest) => 72 result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) 73 rest 74 case Named_Root(root, rest) => 75 result_path ++= JFile.separator 76 result_path ++= JFile.separator 77 result_path ++= root 78 rest 79 case path if path.startsWith("/") => 80 result_path ++= Isabelle_System.cygwin_root() 81 path 82 case path => path 83 } 84 for (p <- space_explode('/', rest) if p != "") { 85 val len = result_path.length 86 if (len > 0 && result_path(len - 1) != JFile.separatorChar) 87 result_path += JFile.separatorChar 88 result_path ++= p 89 } 90 result_path.toString 91 } 92 else standard_path 93 94 def platform_path(path: Path): String = platform_path(standard_path(path)) 95 def platform_file(path: Path): JFile = new JFile(platform_path(path)) 96 97 98 /* platform files */ 99 100 def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile 101 def absolute_name(file: JFile): String = absolute(file).getPath 102 103 def canonical(file: JFile): JFile = file.getCanonicalFile 104 def canonical_name(file: JFile): String = canonical(file).getPath 105 106 def path(file: JFile): Path = Path.explode(standard_path(file)) 107 def pwd(): Path = path(Path.current.absolute_file) 108 109 110 /* relative paths */ 111 112 def relative_path(base: Path, other: Path): Option[Path] = 113 { 114 val base_path = base.file.toPath 115 val other_path = other.file.toPath 116 if (other_path.startsWith(base_path)) 117 Some(path(base_path.relativize(other_path).toFile)) 118 else None 119 } 120 121 122 /* bash path */ 123 124 def bash_path(path: Path): String = Bash.string(standard_path(path)) 125 def bash_path(file: JFile): String = Bash.string(standard_path(file)) 126 127 128 /* directory entries */ 129 130 def check_dir(path: Path): Path = 131 if (path.is_dir) path else error("No such directory: " + path) 132 133 def check_file(path: Path): Path = 134 if (path.is_file) path else error("No such file: " + path) 135 136 137 /* directory content */ 138 139 def read_dir(dir: Path): List[String] = 140 { 141 if (!dir.is_dir) error("No such directory: " + dir.toString) 142 val files = dir.file.listFiles 143 if (files == null) Nil 144 else files.toList.map(_.getName).sorted 145 } 146 147 def find_files( 148 start: JFile, 149 pred: JFile => Boolean = _ => true, 150 include_dirs: Boolean = false, 151 follow_links: Boolean = false): List[JFile] = 152 { 153 val result = new mutable.ListBuffer[JFile] 154 def check(file: JFile) { if (pred(file)) result += file } 155 156 if (start.isFile) check(start) 157 else if (start.isDirectory) { 158 val options = 159 if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) 160 else EnumSet.noneOf(classOf[FileVisitOption]) 161 Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, 162 new SimpleFileVisitor[JPath] { 163 override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = 164 { 165 if (include_dirs) check(path.toFile) 166 FileVisitResult.CONTINUE 167 } 168 override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = 169 { 170 val file = path.toFile 171 if (include_dirs || !file.isDirectory) check(file) 172 FileVisitResult.CONTINUE 173 } 174 } 175 ) 176 } 177 178 result.toList 179 } 180 181 182 /* read */ 183 184 def read(file: JFile): String = Bytes.read(file).text 185 def read(path: Path): String = read(path.file) 186 187 188 def read_stream(reader: BufferedReader): String = 189 { 190 val output = new StringBuilder(100) 191 var c = -1 192 while ({ c = reader.read; c != -1 }) output += c.toChar 193 reader.close 194 output.toString 195 } 196 197 def read_stream(stream: InputStream): String = 198 read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) 199 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) 203 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) 207 208 209 /* read lines */ 210 211 def read_line(reader: BufferedReader): Option[String] = 212 { 213 val line = 214 try { reader.readLine} 215 catch { case _: IOException => null } 216 if (line == null) None else Some(line) 217 } 218 219 def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = 220 { 221 val result = new mutable.ListBuffer[String] 222 var line: Option[String] = None 223 while ({ line = read_line(reader); line.isDefined }) { 224 progress(line.get) 225 result += line.get 226 } 227 reader.close 228 result.toList 229 } 230 231 232 /* write */ 233 234 def writer(file: JFile): BufferedWriter = 235 new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) 236 237 def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) 238 { 239 val stream = make_stream(new FileOutputStream(file)) 240 using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) 241 } 242 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) 245 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) 249 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()) 253 def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = 254 write_xz(path.file, text, options) 255 def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) 256 257 def write_backup(path: Path, text: CharSequence) 258 { 259 if (path.is_file) move(path, path.backup) 260 write(path, text) 261 } 262 263 def write_backup2(path: Path, text: CharSequence) 264 { 265 if (path.is_file) move(path, path.backup2) 266 write(path, text) 267 } 268 269 270 /* append */ 271 272 def append(file: JFile, text: CharSequence): Unit = 273 Files.write(file.toPath, UTF8.bytes(text.toString), 274 StandardOpenOption.APPEND, StandardOpenOption.CREATE) 275 276 def append(path: Path, text: CharSequence): Unit = append(path.file, text) 277 278 279 /* eq */ 280 281 def eq(file1: JFile, file2: JFile): Boolean = 282 try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } 283 catch { case ERROR(_) => false } 284 285 def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) 286 287 288 /* eq_content */ 289 290 def eq_content(file1: JFile, file2: JFile): Boolean = 291 if (eq(file1, file2)) true 292 else if (file1.length != file2.length) false 293 else Bytes.read(file1) == Bytes.read(file2) 294 295 def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) 296 297 298 /* copy */ 299 300 def copy(src: JFile, dst: JFile) 301 { 302 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst 303 if (!eq(src, target)) 304 Files.copy(src.toPath, target.toPath, 305 StandardCopyOption.COPY_ATTRIBUTES, 306 StandardCopyOption.REPLACE_EXISTING) 307 } 308 309 def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) 310 311 312 /* move */ 313 314 def move(src: JFile, dst: JFile) 315 { 316 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst 317 if (!eq(src, target)) 318 Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) 319 } 320 321 def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) 322 323 324 /* symbolic link */ 325 326 def link(src: Path, dst: Path, force: Boolean = false) 327 { 328 val src_file = src.file 329 val dst_file = dst.file 330 val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file 331 332 if (force) target.delete 333 334 try { Files.createSymbolicLink(target.toPath, src_file.toPath) } 335 catch { 336 case _: UnsupportedOperationException if Platform.is_windows => 337 Cygwin.link(standard_path(src), target) 338 case _: FileSystemException if Platform.is_windows => 339 Cygwin.link(standard_path(src), target) 340 } 341 } 342 343 344 /* permissions */ 345 346 def is_executable(path: Path): Boolean = 347 { 348 if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok 349 else path.file.canExecute 350 } 351 352 def set_executable(path: Path, flag: Boolean) 353 { 354 if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) 355 else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) 356 else path.file.setExecutable(flag, false) 357 } 358} 359