src/Pure/General/file.scala
author wenzelm
Fri, 09 Oct 2015 16:29:18 +0200
changeset 61373 16ed9b97c72d
parent 61371 17944b500166
child 61959 364007370bb7
permissions -rw-r--r--
more accurate imitation of "cp -p -f";
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}
61373
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
    13
import java.nio.file.{StandardCopyOption, Files}
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    14
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
    15
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    16
import java.util.regex.Pattern
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    17
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    18
import scala.collection.mutable
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    19
import scala.util.matching.Regex
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    20
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    21
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    22
object File
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    23
{
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    24
  /* standard path (Cygwin or Posix) */
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    25
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    26
  def standard_path(path: Path): String = path.expand.implode
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    27
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    28
  def standard_path(platform_path: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    29
    if (Platform.is_windows) {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    30
      val Platform_Root = new Regex("(?i)" +
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 60992
diff changeset
    31
        Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    32
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    33
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    34
      platform_path.replace('/', '\\') match {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    35
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    36
        case Drive(letter, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    37
          "/cygdrive/" + Word.lowercase(letter) +
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    38
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    39
        case path => path.replace('\\', '/')
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    40
      }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    41
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    42
    else platform_path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    43
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    44
  def standard_path(file: JFile): String = standard_path(file.getPath)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    45
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    46
  def standard_url(name: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    47
    try {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    48
      val url = new URL(name)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    49
      if (url.getProtocol == "file")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    50
        standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    51
      else name
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    52
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    53
    catch { case _: MalformedURLException => standard_path(name) }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    54
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    55
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    56
  /* platform path (Windows or Posix) */
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    57
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    58
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    59
  private val Named_Root = new Regex("//+([^/]*)(.*)")
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    60
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    61
  def platform_path(standard_path: String): String =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    62
    if (Platform.is_windows) {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    63
      val result_path = new StringBuilder
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    64
      val rest =
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    65
        standard_path match {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    66
          case Cygdrive(drive, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    67
            result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    68
            rest
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    69
          case Named_Root(root, rest) =>
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    70
            result_path ++= JFile.separator
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    71
            result_path ++= JFile.separator
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    72
            result_path ++= root
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    73
            rest
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    74
          case path if path.startsWith("/") =>
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 60992
diff changeset
    75
            result_path ++= Isabelle_System.cygwin_root()
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    76
            path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    77
          case path => path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    78
        }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    79
      for (p <- space_explode('/', rest) if p != "") {
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    80
        val len = result_path.length
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    81
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    82
          result_path += JFile.separatorChar
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    83
        result_path ++= p
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    84
      }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    85
      result_path.toString
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    86
    }
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    87
    else standard_path
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    88
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    89
  def platform_path(path: Path): String = platform_path(standard_path(path))
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    90
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    91
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
    92
  def platform_url(raw_path: Path): String =
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    93
  {
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    94
    val path = raw_path.expand
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    95
    require(path.is_absolute)
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    96
    val s = platform_path(path).replaceAll(" ", "%20")
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    97
    if (!Platform.is_windows) "file://" + s
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    98
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
    99
    else "file:///" + s.replace('\\', '/')
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   100
  }
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   101
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   102
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   103
  /* shell path (bash) */
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   104
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   105
  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
60992
89effcb342df clarified modules, like ML version;
wenzelm
parents: 60988
diff changeset
   106
  def shell_path(file: JFile): String = "'" + standard_path(file) + "'"
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   107
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 58610
diff changeset
   108
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   109
  /* directory content */
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   110
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   111
  def read_dir(dir: Path): List[String] =
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   112
  {
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   113
    if (!dir.is_dir) error("Bad directory: " + dir.toString)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   114
    val files = dir.file.listFiles
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   115
    if (files == null) Nil
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   116
    else files.toList.map(_.getName)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   117
  }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   118
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   119
  def find_files(dir: Path): Stream[Path] =
56783
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   120
    read_dir(dir).toStream.map(name =>
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   121
      if (Path.is_wellformed(name)) {
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   122
        val path = dir + Path.basic(name)
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   123
        path #:: (if (path.is_dir) find_files(path) else Stream.empty)
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   124
      }
afaec818fcfd ignore malformed file names outright, e.g. .class files with dollar;
wenzelm
parents: 56428
diff changeset
   125
      else Stream.empty).flatten
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   126
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   127
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   128
  /* read */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   129
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 53336
diff changeset
   130
  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
   131
  def read(path: Path): String = read(path.file)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
   132
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   133
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   134
  def read_stream(reader: BufferedReader): String =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   135
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   136
    val output = new StringBuilder(100)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   137
    var c = -1
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   138
    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
   139
    reader.close
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   140
    output.toString
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   141
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   142
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   143
  def read_stream(stream: InputStream): String =
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   144
   read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   145
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   146
  def read_gzip(file: JFile): String =
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   147
    read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   148
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50203
diff changeset
   149
  def read_gzip(path: Path): String = read_gzip(path.file)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   150
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   151
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   152
  /* read lines */
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   153
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   154
  def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   155
  {
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   156
    val result = new mutable.ListBuffer[String]
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   157
    var line: String = null
51251
d55cce4d72dd more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents: 50845
diff changeset
   158
    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   159
      progress(line)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   160
      result += line
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   161
    }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   162
    reader.close
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   163
    result.toList
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   164
  }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   165
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50684
diff changeset
   166
48550
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   167
  /* try_read */
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   168
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   169
  def try_read(paths: Seq[Path]): String =
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   170
  {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   171
    val buf = new StringBuilder
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   172
    for (path <- paths if path.is_file) {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   173
      buf.append(read(path))
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   174
      buf.append('\n')
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   175
    }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   176
    buf.toString
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   177
  }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   178
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
   179
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   180
  /* write */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   181
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents: 51982
diff changeset
   182
  def write_file(file: JFile, text: Iterable[CharSequence],
51982
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   183
    make_stream: OutputStream => OutputStream)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   184
  {
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   185
    val stream = make_stream(new FileOutputStream(file))
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   186
    val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))
51982
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   187
    try { text.iterator.foreach(writer.append(_)) }
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   188
    finally { writer.close }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   189
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   190
51982
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   191
  def write(file: JFile, text: Iterable[CharSequence]): Unit = write_file(file, text, (s) => s)
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   192
  def write(file: JFile, text: CharSequence): Unit = write(file, List(text))
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   193
  def write(path: Path, text: Iterable[CharSequence]): Unit = write(path.file, text)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   194
  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
   195
51982
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   196
  def write_gzip(file: JFile, text: Iterable[CharSequence]): Unit =
51504
18095684c5a6 basic support for xz files;
wenzelm
parents: 51251
diff changeset
   197
    write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
51982
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   198
  def write_gzip(file: JFile, text: CharSequence): Unit = write_gzip(file, List(text))
fb4352e89022 more scalable File.write via separate chunks;
wenzelm
parents: 51505
diff changeset
   199
  def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
   200
  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
   201
53336
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   202
  def write_backup(path: Path, text: CharSequence)
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   203
  {
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   204
    path.file renameTo path.backup.file
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   205
    File.write(path, text)
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   206
  }
b3bf6d72fea5 more general backup files;
wenzelm
parents: 52671
diff changeset
   207
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   208
  def write_backup2(path: Path, text: CharSequence)
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   209
  {
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   210
    path.file renameTo path.backup2.file
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   211
    File.write(path, text)
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   212
  }
fffdbce036db added update_cartouches tool;
wenzelm
parents: 56783
diff changeset
   213
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   214
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   215
  /* copy */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   216
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   217
  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
   218
    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
   219
    catch { case ERROR(_) => false }
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   220
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   221
  def copy(src: JFile, dst: JFile)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   222
  {
61371
17944b500166 clarified, according to Isabelle_System.copy_file in ML;
wenzelm
parents: 61291
diff changeset
   223
    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
   224
    if (!eq(src, target))
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   225
      Files.copy(src.toPath, target.toPath,
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   226
        StandardCopyOption.COPY_ATTRIBUTES,
16ed9b97c72d more accurate imitation of "cp -p -f";
wenzelm
parents: 61371
diff changeset
   227
        StandardCopyOption.REPLACE_EXISTING)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   228
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   229
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   230
  def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   231
}