src/Pure/System/standard_system.scala

--- a/src/Pure/System/standard_system.scala	Wed Jun 22 21:54:35 2011 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Jun 22 23:56:44 2011 +0200
@@ -13,6 +13,7 @@
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
+import java.nio.charset.Charset
 
 import scala.io.{Source, Codec}
 import scala.util.matching.Regex
@@ -23,7 +24,8 @@
 {
   /* UTF-8 charset */
 
-  val charset = "UTF-8"
+  val charset_name: String = "UTF-8"
+  val charset: Charset = Charset.forName(charset_name)
   def codec(): Codec = Codec(charset)
 
   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
@@ -95,7 +97,8 @@
 
   def write_file(file: File, text: CharSequence)
   {
-    val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
+    val writer =
+      new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
     try { writer.append(text) }
     finally { writer.close }
   }