src/Tools/jEdit/src/isabelle_encoding.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 43695 5130dfe1b7be
child 48277 f14e564fca1a
permissions -rw-r--r--
propagate editor perspective through document model;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/isabelle_encoding.scala
wenzelm@36760
     2
    Author:     Makarius
wenzelm@36760
     3
wenzelm@36760
     4
Isabelle encoding -- based on UTF-8.
wenzelm@36760
     5
*/
wenzelm@34619
     6
wenzelm@34619
     7
package isabelle.jedit
wenzelm@34619
     8
wenzelm@34760
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
wenzelm@34619
    12
import org.gjt.sp.jedit.io.Encoding
wenzelm@34625
    13
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@34619
    14
wenzelm@36015
    15
import java.nio.charset.{Charset, CodingErrorAction}
wenzelm@34620
    16
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
wenzelm@34620
    17
  CharArrayReader, ByteArrayOutputStream}
wenzelm@34620
    18
wenzelm@36015
    19
import scala.io.{Codec, Source, BufferedSource}
wenzelm@34619
    20
wenzelm@34619
    21
wenzelm@34738
    22
object Isabelle_Encoding
wenzelm@34624
    23
{
wenzelm@34624
    24
  val NAME = "UTF-8-Isabelle"
wenzelm@34625
    25
wenzelm@34625
    26
  def is_active(buffer: JEditBuffer): Boolean =
wenzelm@34793
    27
    buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
wenzelm@34624
    28
}
wenzelm@34624
    29
wenzelm@34738
    30
class Isabelle_Encoding extends Encoding
wenzelm@34619
    31
{
wenzelm@43516
    32
  private val BUFSIZE = 32768
wenzelm@34620
    33
wenzelm@36015
    34
  private def text_reader(in: InputStream, codec: Codec): Reader =
wenzelm@34620
    35
  {
wenzelm@36015
    36
    val source = new BufferedSource(in)(codec)
wenzelm@43695
    37
    new CharArrayReader(Symbol.decode(source.mkString).toArray)
wenzelm@34620
    38
  }
wenzelm@34619
    39
wenzelm@37175
    40
  override def getTextReader(in: InputStream): Reader =
wenzelm@36015
    41
    text_reader(in, Standard_System.codec())
wenzelm@34619
    42
wenzelm@37175
    43
  override def getPermissiveTextReader(in: InputStream): Reader =
wenzelm@37175
    44
  {
wenzelm@37175
    45
    val codec = Standard_System.codec()
wenzelm@37175
    46
    codec.onMalformedInput(CodingErrorAction.REPLACE)
wenzelm@37175
    47
    codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
wenzelm@37175
    48
    text_reader(in, codec)
wenzelm@37175
    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@43695
    56
        val text = Symbol.encode(toString(Standard_System.charset_name))
wenzelm@34805
    57
        out.write(text.getBytes(Standard_System.charset))
wenzelm@34620
    58
        out.flush()
wenzelm@34620
    59
      }
wenzelm@34621
    60
      override def close() { out.close() }
wenzelm@34620
    61
    }
wenzelm@43516
    62
    new OutputStreamWriter(buffer, Standard_System.charset.newEncoder())
wenzelm@34620
    63
  }
wenzelm@34619
    64
}