src/Pure/General/file.scala
author wenzelm
Thu, 23 Aug 2012 20:34:51 +0200
changeset 48913 f686cb016c0c
parent 48613 232652ac346e
child 49610 1b36c6676685
permissions -rw-r--r--
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
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,
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    11
  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile}
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    12
import java.util.zip.GZIPOutputStream
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    13
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    14
import scala.collection.mutable
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    15
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    16
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    17
object File
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    18
{
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    19
  /* directory content */
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    20
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    21
  def read_dir(dir: Path): List[String] =
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    22
  {
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    23
    if (!dir.is_dir) error("Bad directory: " + dir.toString)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    24
    val files = dir.file.listFiles
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    25
    if (files == null) Nil
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    26
    else files.toList.map(_.getName)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    27
  }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    28
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    29
  def find_files(dir: Path): Stream[Path] =
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    30
    read_dir(dir).toStream.map(name => {
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    31
      val path = dir + Path.basic(name)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    32
      path #:: (if (path.is_dir) find_files(path) else Stream.empty)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    33
    }).flatten
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    34
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
    35
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    36
  /* read */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    37
48913
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    38
  def read_bytes(file: JFile): Array[Byte] =
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    39
  {
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    40
    var i = 0
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    41
    var m = 0
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    42
    val n = file.length.toInt
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    43
    val buf = new Array[Byte](n)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    44
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    45
    val stream = new FileInputStream(file)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    46
    try {
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    47
      do {
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    48
        m = stream.read(buf, i, n - i)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    49
        if (m != -1) i += m
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    50
      } while (m != -1 && n > i)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    51
    }
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    52
    finally { stream.close }
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    53
    buf
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    54
  }
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    55
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    56
  def read(file: JFile): String =
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    57
    new String(read_bytes(file), Standard_System.charset)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    58
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    59
  def read(path: Path): String = read(path.file)
f686cb016c0c more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents: 48613
diff changeset
    60
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    61
  def read(reader: BufferedReader): String =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    62
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    63
    val output = new StringBuilder(100)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    64
    var c = -1
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    65
    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
    66
    reader.close
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    67
    output.toString
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    68
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    69
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    70
  def read(stream: InputStream): String =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    71
    read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    72
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    73
48550
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    74
  /* try_read */
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    75
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    76
  def try_read(paths: Seq[Path]): String =
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    77
  {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    78
    val buf = new StringBuilder
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    79
    for (path <- paths if path.is_file) {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    80
      buf.append(read(path))
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    81
      buf.append('\n')
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    82
    }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    83
    buf.toString
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    84
  }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    85
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    86
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    87
  /* write */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    88
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    89
  private def write_file(file: JFile, text: CharSequence, gzip: Boolean)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    90
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    91
    val stream1 = new FileOutputStream(file)
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    92
    val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    93
    val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    94
    try { writer.append(text) }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    95
    finally { writer.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    96
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    97
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    98
  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    99
  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
   100
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
   101
  def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
   102
  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
   103
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   104
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   105
  /* copy */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   106
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   107
  def eq(file1: JFile, file2: JFile): Boolean =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   108
    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   109
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   110
  def copy(src: JFile, dst: JFile)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   111
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   112
    if (!eq(src, dst)) {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   113
      val in = new FileInputStream(src)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   114
      try {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   115
        val out = new FileOutputStream(dst)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   116
        try {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   117
          val buf = new Array[Byte](65536)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   118
          var m = 0
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   119
          do {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   120
            m = in.read(buf, 0, buf.length)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   121
            if (m != -1) out.write(buf, 0, m)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   122
          } while (m != -1)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   123
        }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   124
        finally { out.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   125
      }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   126
      finally { in.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   127
    }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   128
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   129
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   130
  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
   131
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   132
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48550
diff changeset
   133
  /* tmp files */
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   134
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   135
  def tmp_file(prefix: String): JFile =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   136
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   137
    val file = JFile.createTempFile(prefix, null)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   138
    file.deleteOnExit
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   139
    file
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   140
  }
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   141
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   142
  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   143
  {
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   144
    val file = tmp_file(prefix)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   145
    try { body(file) } finally { file.delete }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   146
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   147
}
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   148