src/Pure/General/file.scala
author wenzelm
Fri, 27 Jul 2012 14:22:32 +0200
changeset 48550 97592027a2a8
parent 48494 00eb5be9e76b
child 48613 232652ac346e
permissions -rw-r--r--
tuned signature;
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,
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    11
  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
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
{
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    19
  /* read */
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
  def read(reader: BufferedReader): String =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    22
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    23
    val output = new StringBuilder(100)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    24
    var c = -1
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    25
    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
    26
    reader.close
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    27
    output.toString
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    28
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    29
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    30
  def read(stream: InputStream): String =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    31
    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
    32
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    33
  def read(file: JFile): String = read(new FileInputStream(file))
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    34
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    35
  def read(path: Path): String = read(path.file)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    36
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    37
48550
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    38
  /* try_read */
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    39
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    40
  def try_read(paths: Seq[Path]): String =
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    41
  {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    42
    val buf = new StringBuilder
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    43
    for (path <- paths if path.is_file) {
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    44
      buf.append(read(path))
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    45
      buf.append('\n')
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    46
    }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    47
    buf.toString
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    48
  }
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    49
97592027a2a8 tuned signature;
wenzelm
parents: 48494
diff changeset
    50
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    51
  /* write */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    52
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    53
  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
    54
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    55
    val stream1 = new FileOutputStream(file)
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    56
    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
    57
    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
    58
    try { writer.append(text) }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    59
    finally { writer.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    60
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    61
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    62
  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
    63
  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
    64
48494
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    65
  def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
00eb5be9e76b read/write dependency information;
wenzelm
parents: 48418
diff changeset
    66
  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
    67
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
  /* copy */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    70
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    71
  def eq(file1: JFile, file2: JFile): Boolean =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    72
    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
    73
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    74
  def copy(src: JFile, dst: JFile)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    75
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    76
    if (!eq(src, dst)) {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    77
      val in = new FileInputStream(src)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    78
      try {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    79
        val out = new FileOutputStream(dst)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    80
        try {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    81
          val buf = new Array[Byte](65536)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    82
          var m = 0
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    83
          do {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    84
            m = in.read(buf, 0, buf.length)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    85
            if (m != -1) out.write(buf, 0, m)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    86
          } while (m != -1)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    87
        }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    88
        finally { out.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    89
      }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    90
      finally { in.close }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    91
    }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    92
  }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    93
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    94
  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
    95
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
  /* misc */
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
    98
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
    99
  def tmp_file(prefix: String): JFile =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   100
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   101
    val file = JFile.createTempFile(prefix, null)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   102
    file.deleteOnExit
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   103
    file
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   104
  }
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   105
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   106
  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   107
  {
1a634f9614fb some actual build function on ML side;
wenzelm
parents: 48411
diff changeset
   108
    val file = tmp_file(prefix)
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   109
    try { body(file) } finally { file.delete }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   110
  }
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
  // FIXME handle (potentially cyclic) directory graph
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   113
  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   114
  {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   115
    val files = new mutable.ListBuffer[JFile]
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   116
    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   117
    def find_entry(entry: JFile)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   118
    {
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   119
      if (ok(entry)) files += entry
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   120
      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   121
    }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   122
    find_entry(start)
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   123
    files.toList
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff changeset
   124
  }
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