prefer actual charset over charset name;

--- 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 }
   }

--- 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())
   }
 }