# HG changeset patch
# User wenzelm
# Date 1342819014 -7200
# Node ID 5b3440850d366bf915bd45ca39b19a6213c5eff4
# Parent  5539322f68c92dfc8beeeeb4f9f4604306bcd4ff
more abstract file system operations in Scala, corresponding to ML version;

diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/General/file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/file.scala	Fri Jul 20 23:16:54 2012 +0200
@@ -0,0 +1,107 @@
+/*  Title:      Pure/General/file.scala
+    Author:     Makarius
+
+File system operations.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
+  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
+import java.util.zip.GZIPOutputStream
+
+import scala.collection.mutable
+
+
+object File
+{
+  /* read */
+
+  def read(reader: BufferedReader): String =
+  {
+    val output = new StringBuilder(100)
+    var c = -1
+    while ({ c = reader.read; c != -1 }) output += c.toChar
+    reader.close
+    output.toString
+  }
+
+  def read(stream: InputStream): String =
+    read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
+
+  def read(file: JFile): String = read(new FileInputStream(file))
+
+  def read(path: Path): String = read(path.file)
+
+
+  /* write */
+
+  private def write_file(file: JFile, text: CharSequence, zip: Boolean)
+  {
+    val stream1 = new FileOutputStream(file)
+    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
+    val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
+    try { writer.append(text) }
+    finally { writer.close }
+  }
+
+  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
+  def write(path: Path, text: CharSequence): Unit = write(path.file, text)
+
+  def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
+  def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text)
+
+
+  /* copy */
+
+  def eq(file1: JFile, file2: JFile): Boolean =
+    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
+
+  def copy(src: JFile, dst: JFile)
+  {
+    if (!eq(src, dst)) {
+      val in = new FileInputStream(src)
+      try {
+        val out = new FileOutputStream(dst)
+        try {
+          val buf = new Array[Byte](65536)
+          var m = 0
+          do {
+            m = in.read(buf, 0, buf.length)
+            if (m != -1) out.write(buf, 0, m)
+          } while (m != -1)
+        }
+        finally { out.close }
+      }
+      finally { in.close }
+    }
+  }
+
+  def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
+
+
+  /* misc */
+
+  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+  {
+    val file = JFile.createTempFile(prefix, null)
+    file.deleteOnExit
+    try { body(file) } finally { file.delete }
+  }
+
+  // FIXME handle (potentially cyclic) directory graph
+  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
+  {
+    val files = new mutable.ListBuffer[JFile]
+    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
+    def find_entry(entry: JFile)
+    {
+      if (ok(entry)) files += entry
+      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
+    }
+    find_entry(start)
+    files.toList
+  }
+}
+
diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 20 22:39:59 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 23:16:54 2012 +0200
@@ -142,7 +142,7 @@
 
     def parse_entries(root: JFile): List[Session_Entry] =
     {
-      val toks = syntax.scan(Standard_System.read_file(root))
+      val toks = syntax.scan(File.read(root))
       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
@@ -207,8 +207,7 @@
   private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
   {
     val dirs =
-      split_lines(Standard_System.read_file(catalog)).
-        filterNot(line => line == "" || line.startsWith("#"))
+      split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
     (queue /: dirs)((queue1, dir1) =>
       try {
         val dir2 = dir + Path.explode(dir1)
@@ -275,15 +274,12 @@
       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
     {
       Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
-      Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
-        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
-      Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
-        Standard_System.read_file(
-          Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
-        Standard_System.read_file(
-          Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
-        Standard_System.read_file(
-          Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
+      File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
+        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
+      File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
+        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
+        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
+        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
     }
 
     // prepare log dir
@@ -304,10 +300,10 @@
 
           val log = log_dir + Path.basic(key.name)
           if (rc == 0) {
-            Standard_System.write_file(log.ext("gz").file, out, true)
+            File.write_zip(log.ext("gz"), out)
           }
           else {
-            Standard_System.write_file(log.file, out)
+            File.write(log, out)
             echo(key.name + " FAILED")
             echo("(see also " + log.file + ")")
             val lines = split_lines(out)
diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Jul 20 22:39:59 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Jul 20 23:16:54 2012 +0200
@@ -68,7 +68,7 @@
               case Some(path) => path
             }
 
-          Standard_System.with_tmp_file("settings") { dump =>
+          File.with_tmp_file("settings") { dump =>
               val shell_prefix =
                 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
                 else Nil
@@ -78,7 +78,7 @@
               if (rc != 0) error(output)
 
               val entries =
-                (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
+                (for (entry <- File.read(dump) split "\0" if entry != "") yield {
                   val i = entry.indexOf('=')
                   if (i <= 0) (entry -> "")
                   else (entry.substring(0, i) -> entry.substring(i + 1))
@@ -132,7 +132,7 @@
     for {
       path <- paths
       file = platform_file(path) if file.isFile
-    } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
+    } { buf.append(File.read(file)); buf.append('\n') }
     buf.toString
   }
 
@@ -243,13 +243,13 @@
 
   def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
   {
-    Standard_System.with_tmp_file("isabelle_script") { script_file =>
-      Standard_System.write_file(script_file, script)
+    File.with_tmp_file("isabelle_script") { script_file =>
+      File.write(script_file, script)
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
 
       proc.stdin.close
-      val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
-      val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
+      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
+      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
 
       val rc =
         try { proc.join }
diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Jul 20 22:39:59 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 20 23:16:54 2012 +0200
@@ -51,8 +51,7 @@
 
     def parse_entries(file: JFile): List[Options => Options] =
     {
-      val toks = syntax.scan(Standard_System.read_file(file))
-      parse_all(rep(entry), Token.reader(toks, file.toString)) match {
+      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Fri Jul 20 22:39:59 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Fri Jul 20 23:16:54 2012 +0200
@@ -11,15 +11,11 @@
 import java.util.regex.Pattern
 import java.util.Locale
 import java.net.URL
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
-  BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File => JFile, FileFilter, IOException}
+import java.io.{File => JFile}
 import java.nio.charset.Charset
-import java.util.zip.GZIPOutputStream
 
 import scala.io.Codec
 import scala.util.matching.Regex
-import scala.collection.mutable
 
 
 object Standard_System
@@ -100,74 +96,6 @@
   }
 
 
-  /* basic file operations */
-
-  def slurp(reader: BufferedReader): String =
-  {
-    val output = new StringBuilder(100)
-    var c = -1
-    while ({ c = reader.read; c != -1 }) output += c.toChar
-    reader.close
-    output.toString
-  }
-
-  def slurp(stream: InputStream): String =
-    slurp(new BufferedReader(new InputStreamReader(stream, charset)))
-
-  def read_file(file: JFile): String = slurp(new FileInputStream(file))
-
-  def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
-  {
-    val stream1 = new FileOutputStream(file)
-    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
-    val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
-    try { writer.append(text) }
-    finally { writer.close }
-  }
-
-  def eq_file(file1: JFile, file2: JFile): Boolean =
-    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
-
-  def copy_file(src: JFile, dst: JFile) =
-    if (!eq_file(src, dst)) {
-      val in = new FileInputStream(src)
-      try {
-        val out = new FileOutputStream(dst)
-        try {
-          val buf = new Array[Byte](65536)
-          var m = 0
-          do {
-            m = in.read(buf, 0, buf.length)
-            if (m != -1) out.write(buf, 0, m)
-          } while (m != -1)
-        }
-        finally { out.close }
-      }
-      finally { in.close }
-    }
-
-  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
-  {
-    val file = JFile.createTempFile(prefix, null)
-    file.deleteOnExit
-    try { body(file) } finally { file.delete }
-  }
-
-  // FIXME handle (potentially cyclic) directory graph
-  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
-  {
-    val files = new mutable.ListBuffer[JFile]
-    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
-    def find_entry(entry: JFile)
-    {
-      if (ok(entry)) files += entry
-      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
-    }
-    find_entry(start)
-    files.toList
-  }
-
-
   /* shell processes */
 
   def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
@@ -188,7 +116,7 @@
   def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close
-    val output = slurp(proc.getInputStream)
+    val output = File.read(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {
diff -r 5539322f68c9 -r 5b3440850d36 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Jul 20 22:39:59 2012 +0200
+++ b/src/Pure/build-jars	Fri Jul 20 23:16:54 2012 +0200
@@ -14,6 +14,7 @@
   Concurrent/simple_thread.scala
   Concurrent/volatile.scala
   General/exn.scala
+  General/file.scala
   General/graph.scala
   General/linear_set.scala
   General/path.scala