# HG changeset patch
# User wenzelm
# Date 1357135718 -3600
# Node ID 12b7e0b4a66ea1680a0d5a1e2ccb8e63ae6b981f
# Parent  34b109c5324cda086f31f156a990d329d1859d67
support File.read_gzip as well, in accordance to File.write_gzip;
tuned signature;

diff -r 34b109c5324c -r 12b7e0b4a66e src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Jan 02 13:50:59 2013 +0100
+++ b/src/Pure/General/file.scala	Wed Jan 02 15:08:38 2013 +0100
@@ -8,8 +8,9 @@
 
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
-  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile}
-import java.util.zip.GZIPOutputStream
+  InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader,
+  File => JFile}
+import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 
 import scala.collection.mutable
 
@@ -54,10 +55,10 @@
   }
 
   def read(file: JFile): String = new String(read_bytes(file), UTF8.charset)
-
   def read(path: Path): String = read(path.file)
 
-  def read(reader: BufferedReader): String =
+
+  def read_stream(reader: BufferedReader): String =
   {
     val output = new StringBuilder(100)
     var c = -1
@@ -66,8 +67,12 @@
     output.toString
   }
 
-  def read(stream: InputStream): String =
-    read(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
+  def read_stream(stream: InputStream): String =
+   read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
+
+  def read_gzip(file: JFile): String =
+    read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
+  def read_gzip(path: Path): String = read_gzip(path.file)
 
 
   /* try_read */
diff -r 34b109c5324c -r 12b7e0b4a66e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Jan 02 13:50:59 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Jan 02 15:08:38 2013 +0100
@@ -232,7 +232,7 @@
   private def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close
-    val output = File.read(proc.getInputStream)
+    val output = File.read_stream(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {
@@ -336,8 +336,8 @@
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
 
       proc.stdin.close
-      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
-      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
+      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
+      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) }
 
       val rc =
         try { proc.join }