src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,63 +0,0 @@
     1.4 -/*
     1.5 - * Isabelle encoding -- based on utf-8
     1.6 - *
     1.7 - * @author Makarius
     1.8 - */
     1.9 -
    1.10 -package isabelle.jedit
    1.11 -
    1.12 -import org.gjt.sp.jedit.io.Encoding
    1.13 -import org.gjt.sp.jedit.buffer.JEditBuffer
    1.14 -
    1.15 -import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
    1.16 -import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
    1.17 -  CharArrayReader, ByteArrayOutputStream}
    1.18 -
    1.19 -import scala.io.{Source, BufferedSource}
    1.20 -
    1.21 -
    1.22 -object Isabelle_Encoding
    1.23 -{
    1.24 -  val NAME = "UTF-8-Isabelle"
    1.25 -
    1.26 -  def is_active(buffer: JEditBuffer): Boolean =
    1.27 -    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
    1.28 -}
    1.29 -
    1.30 -class Isabelle_Encoding extends Encoding
    1.31 -{
    1.32 -  private val charset = Charset.forName(Isabelle_System.charset)
    1.33 -  private val BUFSIZE = 32768
    1.34 -
    1.35 -  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
    1.36 -  {
    1.37 -    def source(): Source =
    1.38 -      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
    1.39 -    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
    1.40 -  }
    1.41 -
    1.42 -	override def getTextReader(in: InputStream): Reader =
    1.43 -    text_reader(in, charset.newDecoder())
    1.44 -
    1.45 -	override def getPermissiveTextReader(in: InputStream): Reader =
    1.46 -	{
    1.47 -		val decoder = charset.newDecoder()
    1.48 -		decoder.onMalformedInput(CodingErrorAction.REPLACE)
    1.49 -		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
    1.50 -		text_reader(in, decoder)
    1.51 -	}
    1.52 -
    1.53 -  override def getTextWriter(out: OutputStream): Writer =
    1.54 -  {
    1.55 -    val buffer = new ByteArrayOutputStream(BUFSIZE) {
    1.56 -      override def flush()
    1.57 -      {
    1.58 -        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
    1.59 -        out.write(text.getBytes(Isabelle_System.charset))
    1.60 -        out.flush()
    1.61 -      }
    1.62 -      override def close() { out.close() }
    1.63 -    }
    1.64 -		new OutputStreamWriter(buffer, charset.newEncoder())
    1.65 -  }
    1.66 -}