1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/file.scala	Fri Jul 20 23:16:54 2012 +0200
     1.3 @@ -0,0 +1,107 @@
     1.4 +/*  Title:      Pure/General/file.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +File system operations.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
    1.14 +  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
    1.15 +import java.util.zip.GZIPOutputStream
    1.16 +
    1.17 +import scala.collection.mutable
    1.18 +
    1.19 +
    1.20 +object File
    1.21 +{
    1.22 +  /* read */
    1.23 +
    1.24 +  def read(reader: BufferedReader): String =
    1.25 +  {
    1.26 +    val output = new StringBuilder(100)
    1.27 +    var c = -1
    1.28 +    while ({ c = reader.read; c != -1 }) output += c.toChar
    1.29 +    reader.close
    1.30 +    output.toString
    1.31 +  }
    1.32 +
    1.33 +  def read(stream: InputStream): String =
    1.34 +    read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
    1.35 +
    1.36 +  def read(file: JFile): String = read(new FileInputStream(file))
    1.37 +
    1.38 +  def read(path: Path): String = read(path.file)
    1.39 +
    1.40 +
    1.41 +  /* write */
    1.42 +
    1.43 +  private def write_file(file: JFile, text: CharSequence, zip: Boolean)
    1.44 +  {
    1.45 +    val stream1 = new FileOutputStream(file)
    1.46 +    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    1.47 +    val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
    1.48 +    try { writer.append(text) }
    1.49 +    finally { writer.close }
    1.50 +  }
    1.51 +
    1.52 +  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
    1.53 +  def write(path: Path, text: CharSequence): Unit = write(path.file, text)
    1.54 +
    1.55 +  def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
    1.56 +  def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text)
    1.57 +
    1.58 +
    1.59 +  /* copy */
    1.60 +
    1.61 +  def eq(file1: JFile, file2: JFile): Boolean =
    1.62 +    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
    1.63 +
    1.64 +  def copy(src: JFile, dst: JFile)
    1.65 +  {
    1.66 +    if (!eq(src, dst)) {
    1.67 +      val in = new FileInputStream(src)
    1.68 +      try {
    1.69 +        val out = new FileOutputStream(dst)
    1.70 +        try {
    1.71 +          val buf = new Array[Byte](65536)
    1.72 +          var m = 0
    1.73 +          do {
    1.74 +            m = in.read(buf, 0, buf.length)
    1.75 +            if (m != -1) out.write(buf, 0, m)
    1.76 +          } while (m != -1)
    1.77 +        }
    1.78 +        finally { out.close }
    1.79 +      }
    1.80 +      finally { in.close }
    1.81 +    }
    1.82 +  }
    1.83 +
    1.84 +  def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
    1.85 +
    1.86 +
    1.87 +  /* misc */
    1.88 +
    1.89 +  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    1.90 +  {
    1.91 +    val file = JFile.createTempFile(prefix, null)
    1.92 +    file.deleteOnExit
    1.93 +    try { body(file) } finally { file.delete }
    1.94 +  }
    1.95 +
    1.96 +  // FIXME handle (potentially cyclic) directory graph
    1.97 +  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
    1.98 +  {
    1.99 +    val files = new mutable.ListBuffer[JFile]
   1.100 +    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
   1.101 +    def find_entry(entry: JFile)
   1.102 +    {
   1.103 +      if (ok(entry)) files += entry
   1.104 +      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
   1.105 +    }
   1.106 +    find_entry(start)
   1.107 +    files.toList
   1.108 +  }
   1.109 +}
   1.110 +

     2.1 --- a/src/Pure/System/build.scala	Fri Jul 20 22:39:59 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 23:16:54 2012 +0200
     2.3 @@ -142,7 +142,7 @@
     2.4  
     2.5      def parse_entries(root: JFile): List[Session_Entry] =
     2.6      {
     2.7 -      val toks = syntax.scan(Standard_System.read_file(root))
     2.8 +      val toks = syntax.scan(File.read(root))
     2.9        parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
    2.10          case Success(result, _) => result
    2.11          case bad => error(bad.toString)
    2.12 @@ -207,8 +207,7 @@
    2.13    private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
    2.14    {
    2.15      val dirs =
    2.16 -      split_lines(Standard_System.read_file(catalog)).
    2.17 -        filterNot(line => line == "" || line.startsWith("#"))
    2.18 +      split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
    2.19      (queue /: dirs)((queue1, dir1) =>
    2.20        try {
    2.21          val dir2 = dir + Path.explode(dir1)
    2.22 @@ -275,15 +274,12 @@
    2.23        !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
    2.24      {
    2.25        Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
    2.26 -      Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
    2.27 -        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
    2.28 -      Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
    2.29 -        Standard_System.read_file(
    2.30 -          Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
    2.31 -        Standard_System.read_file(
    2.32 -          Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
    2.33 -        Standard_System.read_file(
    2.34 -          Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
    2.35 +      File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
    2.36 +        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
    2.37 +      File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
    2.38 +        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
    2.39 +        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
    2.40 +        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
    2.41      }
    2.42  
    2.43      // prepare log dir
    2.44 @@ -304,10 +300,10 @@
    2.45  
    2.46            val log = log_dir + Path.basic(key.name)
    2.47            if (rc == 0) {
    2.48 -            Standard_System.write_file(log.ext("gz").file, out, true)
    2.49 +            File.write_zip(log.ext("gz"), out)
    2.50            }
    2.51            else {
    2.52 -            Standard_System.write_file(log.file, out)
    2.53 +            File.write(log, out)
    2.54              echo(key.name + " FAILED")
    2.55              echo("(see also " + log.file + ")")
    2.56              val lines = split_lines(out)

     3.1 --- a/src/Pure/System/isabelle_system.scala	Fri Jul 20 22:39:59 2012 +0200
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Fri Jul 20 23:16:54 2012 +0200
     3.3 @@ -68,7 +68,7 @@
     3.4                case Some(path) => path
     3.5              }
     3.6  
     3.7 -          Standard_System.with_tmp_file("settings") { dump =>
     3.8 +          File.with_tmp_file("settings") { dump =>
     3.9                val shell_prefix =
    3.10                  if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
    3.11                  else Nil
    3.12 @@ -78,7 +78,7 @@
    3.13                if (rc != 0) error(output)
    3.14  
    3.15                val entries =
    3.16 -                (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
    3.17 +                (for (entry <- File.read(dump) split "\0" if entry != "") yield {
    3.18                    val i = entry.indexOf('=')
    3.19                    if (i <= 0) (entry -> "")
    3.20                    else (entry.substring(0, i) -> entry.substring(i + 1))
    3.21 @@ -132,7 +132,7 @@
    3.22      for {
    3.23        path <- paths
    3.24        file = platform_file(path) if file.isFile
    3.25 -    } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
    3.26 +    } { buf.append(File.read(file)); buf.append('\n') }
    3.27      buf.toString
    3.28    }
    3.29  
    3.30 @@ -243,13 +243,13 @@
    3.31  
    3.32    def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
    3.33    {
    3.34 -    Standard_System.with_tmp_file("isabelle_script") { script_file =>
    3.35 -      Standard_System.write_file(script_file, script)
    3.36 +    File.with_tmp_file("isabelle_script") { script_file =>
    3.37 +      File.write(script_file, script)
    3.38        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
    3.39  
    3.40        proc.stdin.close
    3.41 -      val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
    3.42 -      val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
    3.43 +      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
    3.44 +      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
    3.45  
    3.46        val rc =
    3.47          try { proc.join }

     4.1 --- a/src/Pure/System/options.scala	Fri Jul 20 22:39:59 2012 +0200
     4.2 +++ b/src/Pure/System/options.scala	Fri Jul 20 23:16:54 2012 +0200
     4.3 @@ -51,8 +51,7 @@
     4.4  
     4.5      def parse_entries(file: JFile): List[Options => Options] =
     4.6      {
     4.7 -      val toks = syntax.scan(Standard_System.read_file(file))
     4.8 -      parse_all(rep(entry), Token.reader(toks, file.toString)) match {
     4.9 +      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
    4.10          case Success(result, _) => result
    4.11          case bad => error(bad.toString)
    4.12        }

     5.1 --- a/src/Pure/System/standard_system.scala	Fri Jul 20 22:39:59 2012 +0200
     5.2 +++ b/src/Pure/System/standard_system.scala	Fri Jul 20 23:16:54 2012 +0200
     5.3 @@ -11,15 +11,11 @@
     5.4  import java.util.regex.Pattern
     5.5  import java.util.Locale
     5.6  import java.net.URL
     5.7 -import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     5.8 -  BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     5.9 -  File => JFile, FileFilter, IOException}
    5.10 +import java.io.{File => JFile}
    5.11  import java.nio.charset.Charset
    5.12 -import java.util.zip.GZIPOutputStream
    5.13  
    5.14  import scala.io.Codec
    5.15  import scala.util.matching.Regex
    5.16 -import scala.collection.mutable
    5.17  
    5.18  
    5.19  object Standard_System
    5.20 @@ -100,74 +96,6 @@
    5.21    }
    5.22  
    5.23  
    5.24 -  /* basic file operations */
    5.25 -
    5.26 -  def slurp(reader: BufferedReader): String =
    5.27 -  {
    5.28 -    val output = new StringBuilder(100)
    5.29 -    var c = -1
    5.30 -    while ({ c = reader.read; c != -1 }) output += c.toChar
    5.31 -    reader.close
    5.32 -    output.toString
    5.33 -  }
    5.34 -
    5.35 -  def slurp(stream: InputStream): String =
    5.36 -    slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    5.37 -
    5.38 -  def read_file(file: JFile): String = slurp(new FileInputStream(file))
    5.39 -
    5.40 -  def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
    5.41 -  {
    5.42 -    val stream1 = new FileOutputStream(file)
    5.43 -    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    5.44 -    val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
    5.45 -    try { writer.append(text) }
    5.46 -    finally { writer.close }
    5.47 -  }
    5.48 -
    5.49 -  def eq_file(file1: JFile, file2: JFile): Boolean =
    5.50 -    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
    5.51 -
    5.52 -  def copy_file(src: JFile, dst: JFile) =
    5.53 -    if (!eq_file(src, dst)) {
    5.54 -      val in = new FileInputStream(src)
    5.55 -      try {
    5.56 -        val out = new FileOutputStream(dst)
    5.57 -        try {
    5.58 -          val buf = new Array[Byte](65536)
    5.59 -          var m = 0
    5.60 -          do {
    5.61 -            m = in.read(buf, 0, buf.length)
    5.62 -            if (m != -1) out.write(buf, 0, m)
    5.63 -          } while (m != -1)
    5.64 -        }
    5.65 -        finally { out.close }
    5.66 -      }
    5.67 -      finally { in.close }
    5.68 -    }
    5.69 -
    5.70 -  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    5.71 -  {
    5.72 -    val file = JFile.createTempFile(prefix, null)
    5.73 -    file.deleteOnExit
    5.74 -    try { body(file) } finally { file.delete }
    5.75 -  }
    5.76 -
    5.77 -  // FIXME handle (potentially cyclic) directory graph
    5.78 -  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
    5.79 -  {
    5.80 -    val files = new mutable.ListBuffer[JFile]
    5.81 -    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
    5.82 -    def find_entry(entry: JFile)
    5.83 -    {
    5.84 -      if (ok(entry)) files += entry
    5.85 -      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    5.86 -    }
    5.87 -    find_entry(start)
    5.88 -    files.toList
    5.89 -  }
    5.90 -
    5.91 -
    5.92    /* shell processes */
    5.93  
    5.94    def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    5.95 @@ -188,7 +116,7 @@
    5.96    def process_output(proc: Process): (String, Int) =
    5.97    {
    5.98      proc.getOutputStream.close
    5.99 -    val output = slurp(proc.getInputStream)
   5.100 +    val output = File.read(proc.getInputStream)
   5.101      val rc =
   5.102        try { proc.waitFor }
   5.103        finally {

     6.1 --- a/src/Pure/build-jars	Fri Jul 20 22:39:59 2012 +0200
     6.2 +++ b/src/Pure/build-jars	Fri Jul 20 23:16:54 2012 +0200
     6.3 @@ -14,6 +14,7 @@
     6.4    Concurrent/simple_thread.scala
     6.5    Concurrent/volatile.scala
     6.6    General/exn.scala
     6.7 +  General/file.scala
     6.8    General/graph.scala
     6.9    General/linear_set.scala
    6.10    General/path.scala