# HG changeset patch # User wenzelm # Date 1308779804 -7200 # Node ID 1c4736b9396a9bfded921485f78d2e4b0fc02dff # Parent 55160cf1e4f658bad962492af4c2932fa98961ce prefer actual charset over charset name; 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 } } diff -r 55160cf1e4f6 -r 1c4736b9396a src/Tools/jEdit/src/isabelle_encoding.scala --- a/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jun 22 21:54:35 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jun 22 23:56:44 2011 +0200 @@ -29,8 +29,7 @@ class Isabelle_Encoding extends Encoding { - private val charset = Charset.forName(Standard_System.charset) - val BUFSIZE = 32768 + private val BUFSIZE = 32768 private def text_reader(in: InputStream, codec: Codec): Reader = { @@ -54,12 +53,12 @@ val buffer = new ByteArrayOutputStream(BUFSIZE) { override def flush() { - val text = Isabelle.system.symbols.encode(toString(Standard_System.charset)) + val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name)) out.write(text.getBytes(Standard_System.charset)) out.flush() } override def close() { out.close() } } - new OutputStreamWriter(buffer, charset.newEncoder()) + new OutputStreamWriter(buffer, Standard_System.charset.newEncoder()) } }