prefer actual charset over charset name;
authorwenzelm
Wed Jun 22 23:56:44 2011 +0200 (2011-06-22)
changeset 435161c4736b9396a
parent 43515 55160cf1e4f6
child 43517 87ec9a1c0f98
prefer actual charset over charset name;
src/Pure/System/standard_system.scala
src/Tools/jEdit/src/isabelle_encoding.scala
     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    }
     2.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Wed Jun 22 21:54:35 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Wed Jun 22 23:56:44 2011 +0200
     2.3 @@ -29,8 +29,7 @@
     2.4  
     2.5  class Isabelle_Encoding extends Encoding
     2.6  {
     2.7 -  private val charset = Charset.forName(Standard_System.charset)
     2.8 -  val BUFSIZE = 32768
     2.9 +  private val BUFSIZE = 32768
    2.10  
    2.11    private def text_reader(in: InputStream, codec: Codec): Reader =
    2.12    {
    2.13 @@ -54,12 +53,12 @@
    2.14      val buffer = new ByteArrayOutputStream(BUFSIZE) {
    2.15        override def flush()
    2.16        {
    2.17 -        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
    2.18 +        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
    2.19          out.write(text.getBytes(Standard_System.charset))
    2.20          out.flush()
    2.21        }
    2.22        override def close() { out.close() }
    2.23      }
    2.24 -    new OutputStreamWriter(buffer, charset.newEncoder())
    2.25 +    new OutputStreamWriter(buffer, Standard_System.charset.newEncoder())
    2.26    }
    2.27  }