src/Tools/jEdit/src/isabelle_encoding.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 43695 5130dfe1b7be
child 48277 f14e564fca1a
permissions -rw-r--r--
more explicit indication of swing thread context;
     1 /*  Title:      Tools/jEdit/src/isabelle_encoding.scala
     2     Author:     Makarius
     3 
     4 Isabelle encoding -- based on UTF-8.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.io.Encoding
    13 import org.gjt.sp.jedit.buffer.JEditBuffer
    14 
    15 import java.nio.charset.{Charset, CodingErrorAction}
    16 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
    17   CharArrayReader, ByteArrayOutputStream}
    18 
    19 import scala.io.{Codec, Source, BufferedSource}
    20 
    21 
    22 object Isabelle_Encoding
    23 {
    24   val NAME = "UTF-8-Isabelle"
    25 
    26   def is_active(buffer: JEditBuffer): Boolean =
    27     buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
    28 }
    29 
    30 class Isabelle_Encoding extends Encoding
    31 {
    32   private val BUFSIZE = 32768
    33 
    34   private def text_reader(in: InputStream, codec: Codec): Reader =
    35   {
    36     val source = new BufferedSource(in)(codec)
    37     new CharArrayReader(Symbol.decode(source.mkString).toArray)
    38   }
    39 
    40   override def getTextReader(in: InputStream): Reader =
    41     text_reader(in, Standard_System.codec())
    42 
    43   override def getPermissiveTextReader(in: InputStream): Reader =
    44   {
    45     val codec = Standard_System.codec()
    46     codec.onMalformedInput(CodingErrorAction.REPLACE)
    47     codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
    48     text_reader(in, codec)
    49   }
    50 
    51   override def getTextWriter(out: OutputStream): Writer =
    52   {
    53     val buffer = new ByteArrayOutputStream(BUFSIZE) {
    54       override def flush()
    55       {
    56         val text = Symbol.encode(toString(Standard_System.charset_name))
    57         out.write(text.getBytes(Standard_System.charset))
    58         out.flush()
    59       }
    60       override def close() { out.close() }
    61     }
    62     new OutputStreamWriter(buffer, Standard_System.charset.newEncoder())
    63   }
    64 }