src/Pure/System/standard_system.scala
changeset 43516 1c4736b9396a
parent 39732 4dbc72759706
child 43520 cec9b95fa35d
     1.1 --- a/src/Pure/System/standard_system.scala	Wed Jun 22 21:54:35 2011 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Wed Jun 22 23:56:44 2011 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     1.5    BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.6    File, FileFilter, IOException}
     1.7 +import java.nio.charset.Charset
     1.8  
     1.9  import scala.io.{Source, Codec}
    1.10  import scala.util.matching.Regex
    1.11 @@ -23,7 +24,8 @@
    1.12  {
    1.13    /* UTF-8 charset */
    1.14  
    1.15 -  val charset = "UTF-8"
    1.16 +  val charset_name: String = "UTF-8"
    1.17 +  val charset: Charset = Charset.forName(charset_name)
    1.18    def codec(): Codec = Codec(charset)
    1.19  
    1.20    def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    1.21 @@ -95,7 +97,8 @@
    1.22  
    1.23    def write_file(file: File, text: CharSequence)
    1.24    {
    1.25 -    val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
    1.26 +    val writer =
    1.27 +      new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
    1.28      try { writer.append(text) }
    1.29      finally { writer.close }
    1.30    }