src/Pure/System/standard_system.scala
changeset 48373 527e2bad7cca
parent 48359 e544dbcdf097
child 48409 0d2114eb412a
     1.1 --- a/src/Pure/System/standard_system.scala	Fri Jul 20 18:50:33 2012 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Fri Jul 20 21:04:03 2012 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.5    File, FileFilter, IOException}
     1.6  import java.nio.charset.Charset
     1.7 +import java.util.zip.GZIPOutputStream
     1.8  
     1.9  import scala.io.Codec
    1.10  import scala.util.matching.Regex
    1.11 @@ -115,10 +116,11 @@
    1.12  
    1.13    def read_file(file: File): String = slurp(new FileInputStream(file))
    1.14  
    1.15 -  def write_file(file: File, text: CharSequence)
    1.16 +  def write_file(file: File, text: CharSequence, zip: Boolean = false)
    1.17    {
    1.18 -    val writer =
    1.19 -      new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
    1.20 +    val stream1 = new FileOutputStream(file)
    1.21 +    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    1.22 +    val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
    1.23      try { writer.append(text) }
    1.24      finally { writer.close }
    1.25    }