diff -r 55160cf1e4f6 -r 1c4736b9396a 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 } }