src/Tools/jEdit/src/jedit/isabelle_encoding.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
wenzelm@34619
     1
/*
wenzelm@34619
     2
 * Isabelle encoding -- based on utf-8
wenzelm@34619
     3
 *
wenzelm@34619
     4
 * @author Makarius
wenzelm@34619
     5
 */
wenzelm@34619
     6
wenzelm@34619
     7
package isabelle.jedit
wenzelm@34619
     8
wenzelm@34760
     9
wenzelm@34619
    10
import org.gjt.sp.jedit.io.Encoding
wenzelm@34625
    11
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@34619
    12
wenzelm@34620
    13
import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
wenzelm@34620
    14
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
wenzelm@34620
    15
  CharArrayReader, ByteArrayOutputStream}
wenzelm@34620
    16
wenzelm@34620
    17
import scala.io.{Source, BufferedSource}
wenzelm@34619
    18
wenzelm@34619
    19
wenzelm@34738
    20
object Isabelle_Encoding
wenzelm@34624
    21
{
wenzelm@34624
    22
  val NAME = "UTF-8-Isabelle"
wenzelm@34625
    23
wenzelm@34625
    24
  def is_active(buffer: JEditBuffer): Boolean =
wenzelm@34625
    25
    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
wenzelm@34624
    26
}
wenzelm@34624
    27
wenzelm@34738
    28
class Isabelle_Encoding extends Encoding
wenzelm@34619
    29
{
wenzelm@34619
    30
  private val charset = Charset.forName(Isabelle_System.charset)
wenzelm@34620
    31
  private val BUFSIZE = 32768
wenzelm@34620
    32
wenzelm@34620
    33
  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
wenzelm@34620
    34
  {
wenzelm@34620
    35
    def source(): Source =
wenzelm@34620
    36
      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
wenzelm@34621
    37
    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
wenzelm@34620
    38
  }
wenzelm@34619
    39
wenzelm@34619
    40
	override def getTextReader(in: InputStream): Reader =
wenzelm@34620
    41
    text_reader(in, charset.newDecoder())
wenzelm@34619
    42
wenzelm@34619
    43
	override def getPermissiveTextReader(in: InputStream): Reader =
wenzelm@34619
    44
	{
wenzelm@34619
    45
		val decoder = charset.newDecoder()
wenzelm@34619
    46
		decoder.onMalformedInput(CodingErrorAction.REPLACE)
wenzelm@34619
    47
		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
wenzelm@34620
    48
		text_reader(in, decoder)
wenzelm@34619
    49
	}
wenzelm@34620
    50
wenzelm@34620
    51
  override def getTextWriter(out: OutputStream): Writer =
wenzelm@34620
    52
  {
wenzelm@34620
    53
    val buffer = new ByteArrayOutputStream(BUFSIZE) {
wenzelm@34620
    54
      override def flush()
wenzelm@34620
    55
      {
wenzelm@34620
    56
        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
wenzelm@34620
    57
        out.write(text.getBytes(Isabelle_System.charset))
wenzelm@34620
    58
        out.flush()
wenzelm@34620
    59
      }
wenzelm@34621
    60
      override def close() { out.close() }
wenzelm@34620
    61
    }
wenzelm@34620
    62
		new OutputStreamWriter(buffer, charset.newEncoder())
wenzelm@34620
    63
  }
wenzelm@34619
    64
}