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