src/Pure/General/file.scala
author wenzelm
Sat, 22 Oct 2016 16:39:27 +0200
changeset 64345 b89c29ea208f
parent 64304 96bc94c87a81
child 64482 43f6c28ff496
permissions -rw-r--r--
permissive rename operation (amending b265dd04d57d);
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
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
     4
File system operations.
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}
62703
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
    13
import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
    14
  Files, SimpleFileVisitor, 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
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    16
import java.net.{URL, URLDecoder, 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}
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    18
import java.util.regex.Pattern
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
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    23
import scala.util.matching.Regex
48411
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
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    26
object File
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    27
{
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    28
  /* standard path (Cygwin or Posix) */
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    29
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    30
  def standard_path(path: Path): String = path.expand.implode
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    31
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    32
  def standard_path(platform_path: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    33
    if (Platform.is_windows) {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    34
      val Platform_Root = new Regex("(?i)" +
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 60992
diff changeset
    35
        Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    36
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    37
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    38
      platform_path.replace('/', '\\') match {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    39
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    40
        case Drive(letter, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    41
          "/cygdrive/" + Word.lowercase(letter) +
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    42
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    43
        case path => path.replace('\\', '/')
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
    else platform_path
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 standard_path(file: JFile): String = standard_path(file.getPath)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    49
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64214
diff changeset
    50
  def path(file: JFile): Path = Path.explode(standard_path(file))
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64214
diff changeset
    51
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    52
  def standard_url(name: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    53
    try {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    54
      val url = new URL(name)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    55
      if (url.getProtocol == "file")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    56
        standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    57
      else name
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    58
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    59
    catch { case _: MalformedURLException => standard_path(name) }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    60
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    61
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    62
  /* platform path (Windows or Posix) */
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    63
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    64
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    65
  private val Named_Root = new Regex("//+([^/]*)(.*)")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    66
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    67
  def platform_path(standard_path: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    68
    if (Platform.is_windows) {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    69
      val result_path = new StringBuilder
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    70
      val rest =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    71
        standard_path match {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    72
          case Cygdrive(drive, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    73
            result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    74
            rest
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    75
          case Named_Root(root, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    76
            result_path ++= JFile.separator
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    77
            result_path ++= JFile.separator
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    78
            result_path ++= root
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    79
            rest
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    80
          case path if path.startsWith("/") =>
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 60992
diff changeset
    81
            result_path ++= Isabelle_System.cygwin_root()
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    82
            path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    83
          case path => path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    84
        }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    85
      for (p <- space_explode('/', rest) if p != "") {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    86
        val len = result_path.length
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    87
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    88
          result_path += JFile.separatorChar
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    89
        result_path ++= p
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    90
      }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    91
      result_path.toString
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    92
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    93
    else standard_path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    94
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    95
  def platform_path(path: Path): String = platform_path(standard_path(path))
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    96
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    97
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    98
  def platform_url(raw_path: Path): String =
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    99
  {
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   100
    val path = raw_path.expand
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   101
    require(path.is_absolute)
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   102
    val s = platform_path(path).replaceAll(" ", "%20")
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   103
    if (!Platform.is_windows) "file://" + s
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   104
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   105
    else "file:///" + s.replace('\\', '/')
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   106
  }
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   107
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   108
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
   109
  /* bash path */
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   110
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64220
diff changeset
   111
  def bash_path(path: Path): String = Bash.string(standard_path(path))
96bc94c87a81 clarified modules;
wenzelm
parents: 64220
diff changeset
   112
  def bash_path(file: JFile): String = Bash.string(standard_path(file))
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   113
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   114
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   115
  /* directory entries */
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   116
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   117
  def check_dir(path: Path): Path =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   118
    if (path.is_dir) path else error("No such directory: " + path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   119
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   120
  def check_file(path: Path): Path =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   121
    if (path.is_file) path else error("No such file: " + path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   122
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents: 62444
diff changeset
   123
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   124
  /* directory content */
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   125
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   126
  def read_dir(dir: Path): List[String] =
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   127
  {
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   128
    if (!dir.is_dir) error("Bad directory: " + dir.toString)
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   129
    val files = dir.file.listFiles
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   130
    if (files == null) Nil
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   131
    else files.toList.map(_.getName)
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62704
diff changeset
   132
  }
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   133
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   134
  def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   135
  {
62443
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   136
    val result = new mutable.ListBuffer[JFile]
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   137
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   138
    if (start.isFile && pred(start)) result += start
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   139
    else if (start.isDirectory) {
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   140
      Files.walkFileTree(start.toPath,
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   141
        new SimpleFileVisitor[JPath] {
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   142
          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
   143
          {
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   144
            val file = path.toFile
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   145
            if (pred(file)) result += file
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   146
            FileVisitResult.CONTINUE
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   147
          }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   148
        }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   149
      )
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   150
    }
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   151
133f65ac17e5 just one File.find_files, based on Java 7 Files operations;
wenzelm
parents: 62294
diff changeset
   152
    result.toList
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   153
  }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   154
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   155
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   156
  /* read */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   157
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 53336
diff changeset
   158
  def read(file: JFile): String = Bytes.read(file).toString
48913
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
   159
  def read(path: Path): String = read(path.file)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
   160
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   161
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   162
  def read_stream(reader: BufferedReader): String =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   163
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   164
    val output = new StringBuilder(100)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   165
    var c = -1
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   166
    while ({ c = reader.read; c != -1 }) output += c.toChar
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   167
    reader.close
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   168
    output.toString
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   169
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   170
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   171
  def read_stream(stream: InputStream): String =
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   172
    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
   173
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   174
  def read_gzip(file: JFile): String =
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   175
    read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   176
  def read_gzip(path: Path): String = read_gzip(path.file)
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   177
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   178
  def read_xz(file: JFile): String =
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   179
    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   180
  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
   181
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   182
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   183
  /* read lines */
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   184
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]
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   188
    var line: String = null
51251
d55cce4d72dd more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents: 50845
diff changeset
   189
    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   190
      progress(line)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   191
      result += line
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   192
    }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   193
    reader.close
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
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   200
  def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   201
  {
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   202
    val stream = make_stream(new FileOutputStream(file))
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   203
    val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   204
    try { writer.append(text) } finally { writer.close }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   205
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   206
64003
73af1d36aeff tuned signature;
wenzelm
parents: 64002
diff changeset
   207
  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   208
  def write(path: Path, text: CharSequence): Unit = write(path.file, text)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   209
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   210
  def write_gzip(file: JFile, text: CharSequence): Unit =
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   211
    write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
   212
  def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   213
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   214
  def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
64003
73af1d36aeff tuned signature;
wenzelm
parents: 64002
diff changeset
   215
    File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
73af1d36aeff tuned signature;
wenzelm
parents: 64002
diff changeset
   216
  def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   217
  def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
   218
    write_xz(path.file, text, options)
64003
73af1d36aeff tuned signature;
wenzelm
parents: 64002
diff changeset
   219
  def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
64000
445b3deced8f clarified modules;
wenzelm
parents: 62854
diff changeset
   220
53336
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   221
  def write_backup(path: Path, text: CharSequence)
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   222
  {
64345
b89c29ea208f permissive rename operation (amending b265dd04d57d);
wenzelm
parents: 64304
diff changeset
   223
    if (path.is_file) mv(path, path.backup)
62444
wenzelm
parents: 62443
diff changeset
   224
    write(path, text)
53336
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   225
  }
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   226
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   227
  def write_backup2(path: Path, text: CharSequence)
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   228
  {
64345
b89c29ea208f permissive rename operation (amending b265dd04d57d);
wenzelm
parents: 64304
diff changeset
   229
    if (path.is_file) mv(path, path.backup2)
62444
wenzelm
parents: 62443
diff changeset
   230
    write(path, text)
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   231
  }
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   232
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   233
62703
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   234
  /* append */
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   235
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   236
  def append(file: JFile, text: CharSequence): Unit =
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   237
    Files.write(file.toPath, UTF8.bytes(text.toString),
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   238
      StandardOpenOption.APPEND, StandardOpenOption.CREATE)
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   239
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   240
  def append(path: Path, text: CharSequence): Unit = append(path.file, text)
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   241
01b71da798dd more operations;
wenzelm
parents: 62636
diff changeset
   242
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   243
  /* eq */
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   244
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   245
  def eq(file1: JFile, file2: JFile): Boolean =
49673
2a088cff1e7b more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents: 49610
diff changeset
   246
    try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
2a088cff1e7b more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents: 49610
diff changeset
   247
    catch { case ERROR(_) => false }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   248
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   249
  def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   250
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   251
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   252
  /* copy */
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   253
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   254
  def copy(src: JFile, dst: JFile)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   255
  {
61371
17944b500166 clarified, according to Isabelle_System.copy_file in ML;
wenzelm
parents: 61291
diff changeset
   256
    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
61373
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   257
    if (!eq(src, target))
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   258
      Files.copy(src.toPath, target.toPath,
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   259
        StandardCopyOption.COPY_ATTRIBUTES,
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   260
        StandardCopyOption.REPLACE_EXISTING)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   261
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   262
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   263
  def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   264
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   265
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   266
  /* move */
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   267
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   268
  def mv(file1: JFile, file2: JFile): Unit =
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   269
    Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING)
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   270
b265dd04d57d clarified file operations;
wenzelm
parents: 64003
diff changeset
   271
  def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   272
}