src/Pure/General/file.scala
author wenzelm
Wed, 30 Jun 2021 13:25:35 +0200
changeset 73900 1f1e490dd251
parent 73660 ff716ecb0805
child 73904 51f510517aa0
permissions -rw-r--r--
clarified modules; avoid initial use of _settings during init;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/file.scala
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     3
64698
e022a69db531 tuned comments;
wenzelm
parents: 64668
diff changeset
     4
File-system operations.
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     5
*/
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     6
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     7
package isabelle
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     8
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     9
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    10
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
    11
  OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
    12
  InputStreamReader, File => JFile, IOException}
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72698
diff changeset
    13
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72698
diff changeset
    14
  FileVisitOption, FileVisitResult}
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
    15
import java.nio.file.attribute.BasicFileAttributes
64775
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64760
diff changeset
    16
import java.net.{URL, MalformedURLException}
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
    17
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
69293
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
    18
import java.util.EnumSet
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    19
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    20
import org.tukaani.xz.{XZInputStream, XZOutputStream}
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    21
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    22
import scala.collection.mutable
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    23
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    24
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    25
object File
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    26
{
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    27
  /* standard path (Cygwin or Posix) */
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    28
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    29
  def standard_path(path: Path): String = path.expand.implode
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    30
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    31
  def standard_path(platform_path: String): String =
73900
1f1e490dd251 clarified modules;
wenzelm
parents: 73660
diff changeset
    32
    Isabelle_Env.standard_path(Isabelle_System.cygwin_root(), platform_path)
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    33
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    34
  def standard_path(file: JFile): String = standard_path(file.getPath)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    35
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    36
  def standard_url(name: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    37
    try {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    38
      val url = new URL(name)
64775
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64760
diff changeset
    39
      if (url.getProtocol == "file" && Url.is_wellformed_file(name))
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64760
diff changeset
    40
        standard_path(Url.parse_file(name))
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    41
      else name
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    42
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    43
    catch { case _: MalformedURLException => standard_path(name) }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    44
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    45
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    46
  /* platform path (Windows or Posix) */
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    47
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    48
  def platform_path(standard_path: String): String =
73900
1f1e490dd251 clarified modules;
wenzelm
parents: 73660
diff changeset
    49
    Isabelle_Env.platform_path(Isabelle_System.cygwin_root(), standard_path)
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    50
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    51
  def platform_path(path: Path): String = platform_path(standard_path(path))
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    52
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    53
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    54
66232
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    55
  /* platform files */
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    56
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    57
  def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
66233
7188967253e5 more operations;
wenzelm
parents: 66232
diff changeset
    58
  def absolute_name(file: JFile): String = absolute(file).getPath
7188967253e5 more operations;
wenzelm
parents: 66232
diff changeset
    59
66232
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    60
  def canonical(file: JFile): JFile = file.getCanonicalFile
66233
7188967253e5 more operations;
wenzelm
parents: 66232
diff changeset
    61
  def canonical_name(file: JFile): String = canonical(file).getPath
66232
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    62
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    63
  def path(file: JFile): Path = Path.explode(standard_path(file))
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    64
  def pwd(): Path = path(Path.current.absolute_file)
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    65
be0ab4b94c62 clarified signature;
wenzelm
parents: 65589
diff changeset
    66
66693
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    67
  /* relative paths */
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    68
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    69
  def relative_path(base: Path, other: Path): Option[Path] =
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    70
  {
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    71
    val base_path = base.file.toPath
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    72
    val other_path = other.file.toPath
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    73
    if (other_path.startsWith(base_path))
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    74
      Some(path(base_path.relativize(other_path).toFile))
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    75
    else None
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    76
  }
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    77
02588021b581 more operations;
wenzelm
parents: 66233
diff changeset
    78
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
    79
  /* bash path */
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    80
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64220
diff changeset
    81
  def bash_path(path: Path): String = Bash.string(standard_path(path))
96bc94c87a81 clarified modules;
wenzelm
parents: 64220
diff changeset
    82
  def bash_path(file: JFile): String = Bash.string(standard_path(file))
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    83
72036
e48a5b6b7554 clarified signature;
wenzelm
parents: 71601
diff changeset
    84
  def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
e48a5b6b7554 clarified signature;
wenzelm
parents: 71601
diff changeset
    85
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    86
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    87
  /* directory entries */
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    88
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    89
  def check_dir(path: Path): Path =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    90
    if (path.is_dir) path else error("No such directory: " + path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    91
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    92
  def check_file(path: Path): Path =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    93
    if (path.is_file) path else error("No such file: " + path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    94
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
    95
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
    96
  /* directory content */
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
    97
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
    98
  def read_dir(dir: Path): List[String] =
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
    99
  {
69300
8b6ab9989bcd is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents: 69299
diff changeset
   100
    if (!dir.is_dir) error("No such directory: " + dir.toString)
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   101
    val files = dir.file.listFiles
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   102
    if (files == null) Nil
69427
ff2f39a221d4 clarified operations: uniform sorting of results;
wenzelm
parents: 69405
diff changeset
   103
    else files.toList.map(_.getName).sorted
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   104
  }
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   105
72442
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   106
  def get_dir(dir: Path): String =
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   107
    read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   108
      case List(entry) => entry
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   109
      case dirs =>
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   110
        error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   111
    }
90868036d693 clarified signature;
wenzelm
parents: 72378
diff changeset
   112
64932
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   113
  def find_files(
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   114
    start: JFile,
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   115
    pred: JFile => Boolean = _ => true,
69293
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
   116
    include_dirs: Boolean = false,
69299
2fd070377c99 clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents: 69293
diff changeset
   117
    follow_links: Boolean = false): List[JFile] =
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   118
  {
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   119
    val result = new mutable.ListBuffer[JFile]
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73318
diff changeset
   120
    def check(file: JFile): Unit = if (pred(file)) result += file
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   121
64932
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   122
    if (start.isFile) check(start)
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   123
    else if (start.isDirectory) {
69293
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
   124
      val options =
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
   125
        if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
   126
        else EnumSet.noneOf(classOf[FileVisitOption])
72a9860f8602 clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents: 66693
diff changeset
   127
      Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   128
        new SimpleFileVisitor[JPath] {
64932
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   129
          override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   130
          {
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   131
            if (include_dirs) check(path.toFile)
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   132
            FileVisitResult.CONTINUE
89c0896a19ad clarified operation: include dirs as well;
wenzelm
parents: 64775
diff changeset
   133
          }
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   134
          override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   135
          {
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   136
            val file = path.toFile
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   137
            if (include_dirs || !file.isDirectory) check(file)
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   138
            FileVisitResult.CONTINUE
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   139
          }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   140
        }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   141
      )
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   142
    }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   143
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   144
    result.toList
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   145
  }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   146
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   147
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   148
  /* read */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   149
65589
f70c617e9c26 more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;
wenzelm
parents: 64934
diff changeset
   150
  def read(file: JFile): String = Bytes.read(file).text
48913
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
   151
  def read(path: Path): String = read(path.file)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
   152
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   153
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   154
  def read_stream(reader: BufferedReader): String =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   155
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   156
    val output = new StringBuilder(100)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   157
    var c = -1
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   158
    while ({ c = reader.read; c != -1 }) output += c.toChar
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   159
    reader.close()
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   160
    output.toString
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   161
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   162
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   163
  def read_stream(stream: InputStream): String =
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   164
    read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   165
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   166
  def read_gzip(file: JFile): String =
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   167
    read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   168
  def read_gzip(path: Path): String = read_gzip(path.file)
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   169
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   170
  def read_xz(file: JFile): String =
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   171
    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   172
  def read_xz(path: Path): String = read_xz(path.file)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   173
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   174
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   175
  /* read lines */
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   176
69487
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   177
  def read_line(reader: BufferedReader): Option[String] =
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   178
  {
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   179
    val line =
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   180
      try { reader.readLine}
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   181
      catch { case _: IOException => null }
72698
6f83f7892317 clarified: more uniform;
wenzelm
parents: 72572
diff changeset
   182
    Option(line).map(Library.trim_line)
69487
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   183
  }
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   184
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   185
  def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   186
  {
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   187
    val result = new mutable.ListBuffer[String]
69487
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   188
    var line: Option[String] = None
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   189
    while ({ line = read_line(reader); line.isDefined }) {
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   190
      progress(line.get)
681760f50723 clarified signature;
wenzelm
parents: 69427
diff changeset
   191
      result += line.get
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   192
    }
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   193
    reader.close()
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   194
    result.toList
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   195
  }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   196
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   197
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   198
  /* write */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   199
71534
f10bffaa2bae more scalable output of YXML files;
wenzelm
parents: 71377
diff changeset
   200
  def writer(file: JFile): BufferedWriter =
f10bffaa2bae more scalable output of YXML files;
wenzelm
parents: 71377
diff changeset
   201
    new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
f10bffaa2bae more scalable output of YXML files;
wenzelm
parents: 71377
diff changeset
   202
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73318
diff changeset
   203
  def write_file(
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   204
    file: JFile, text: String, make_stream: OutputStream => OutputStream): Unit =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   205
  {
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   206
    val stream = make_stream(new FileOutputStream(file))
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69301
diff changeset
   207
    using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   208
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   209
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   210
  def write(file: JFile, text: String): Unit = write_file(file, text, s => s)
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   211
  def write(path: Path, text: String): Unit = write(path.file, text)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   212
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   213
  def write_gzip(file: JFile, text: String): Unit =
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   214
    write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   215
  def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   216
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   217
  def write_xz(file: JFile, text: String, options: XZ.Options): Unit =
64003
73af1d36aeff tuned signature;
wenzelm
parents: 64002
diff changeset
   218
    File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   219
  def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options())
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   220
  def write_xz(path: Path, text: String, options: XZ.Options): Unit =
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   221
    write_xz(path.file, text, options)
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   222
  def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   223
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   224
  def write_backup(path: Path, text: String): Unit =
53336
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   225
  {
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72698
diff changeset
   226
    if (path.is_file) Isabelle_System.move_file(path, path.backup)
62444
wenzelm
parents: 62443
diff changeset
   227
    write(path, text)
53336
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   228
  }
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   229
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   230
  def write_backup2(path: Path, text: String): Unit =
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   231
  {
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72698
diff changeset
   232
    if (path.is_file) Isabelle_System.move_file(path, path.backup2)
62444
wenzelm
parents: 62443
diff changeset
   233
    write(path, text)
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   234
  }
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   235
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   236
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72036
diff changeset
   237
  /* change */
075f3cbc7546 clarified signature;
wenzelm
parents: 72036
diff changeset
   238
73627
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   239
  def change(file: JFile, f: String => String): Unit =
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   240
  {
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   241
    val x = read(file)
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   242
    val y = f(x)
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   243
    if (x != y) write(file, y)
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   244
  }
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   245
73660
ff716ecb0805 put more resources into jedit_build component;
wenzelm
parents: 73627
diff changeset
   246
  def change_lines(file: JFile, f: List[String] => List[String]): Unit =
ff716ecb0805 put more resources into jedit_build component;
wenzelm
parents: 73627
diff changeset
   247
    change(file, text => cat_lines(f(split_lines(text))))
ff716ecb0805 put more resources into jedit_build component;
wenzelm
parents: 73627
diff changeset
   248
73627
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   249
  def change(path: Path, f: String => String): Unit = change(path.file, f)
73660
ff716ecb0805 put more resources into jedit_build component;
wenzelm
parents: 73627
diff changeset
   250
  def change_lines(path: Path, f: List[String] => List[String]): Unit = change_lines(path.file, f)
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72036
diff changeset
   251
075f3cbc7546 clarified signature;
wenzelm
parents: 72036
diff changeset
   252
62703
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   253
  /* append */
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   254
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   255
  def append(file: JFile, text: String): Unit =
73627
27659455c592 clarified signature;
wenzelm
parents: 73574
diff changeset
   256
    Files.write(file.toPath, UTF8.bytes(text),
62703
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   257
      StandardOpenOption.APPEND, StandardOpenOption.CREATE)
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   258
73574
12b3f78dde61 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents: 73367
diff changeset
   259
  def append(path: Path, text: String): Unit = append(path.file, text)
62703
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   260
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   261
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   262
  /* eq */
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   263
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   264
  def eq(file1: JFile, file2: JFile): Boolean =
73318
wenzelm
parents: 73317
diff changeset
   265
    try { Files.isSameFile(file1.toPath, file2.toPath) }
49673
2a088cff1e7b more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents: 49610
diff changeset
   266
    catch { case ERROR(_) => false }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   267
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   268
  def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   269
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   270
64934
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   271
  /* eq_content */
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   272
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   273
  def eq_content(file1: JFile, file2: JFile): Boolean =
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   274
    if (eq(file1, file2)) true
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   275
    else if (file1.length != file2.length) false
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   276
    else Bytes.read(file1) == Bytes.read(file2)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   277
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   278
  def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   279
795055a0be98 hardlink within JVM;
wenzelm
parents: 64932
diff changeset
   280
69405
22428643351f more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents: 69402
diff changeset
   281
  /* permissions */
22428643351f more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents: 69402
diff changeset
   282
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   283
  def is_executable(path: Path): Boolean =
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   284
  {
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   285
    if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   286
    else path.file.canExecute
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   287
  }
c175499a7537 added executable flag for exports;
wenzelm
parents: 69487
diff changeset
   288
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73318
diff changeset
   289
  def set_executable(path: Path, flag: Boolean): Unit =
69405
22428643351f more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents: 69402
diff changeset
   290
  {
71114
6cfec8029831 clarified signature;
wenzelm
parents: 69789
diff changeset
   291
    if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
6cfec8029831 clarified signature;
wenzelm
parents: 69789
diff changeset
   292
    else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
69789
2c3e5e58d93f more thorough File.set_executable, notably for Windows;
wenzelm
parents: 69788
diff changeset
   293
    else path.file.setExecutable(flag, false)
69405
22428643351f more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents: 69402
diff changeset
   294
  }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   295
}