src/Tools/jEdit/src/jedit/IsabelleEncoding.scala
author wenzelm
Fri, 26 Jun 2009 20:07:34 +0200
changeset 34625 799a40faa4f1
parent 34624 5e4f33d033ba
permissions -rw-r--r--
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     1
/*
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     2
 * Isabelle encoding -- based on utf-8
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     3
 *
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     4
 * @author Makarius
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     5
 */
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     6
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     8
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     9
import org.gjt.sp.jedit.io.Encoding
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    10
import org.gjt.sp.jedit.buffer.JEditBuffer
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    11
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    12
import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    13
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    14
  CharArrayReader, ByteArrayOutputStream}
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    15
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    16
import scala.io.{Source, BufferedSource}
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    17
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    18
34624
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    19
object IsabelleEncoding
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    20
{
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    21
  val NAME = "UTF-8-Isabelle"
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    22
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    23
  def is_active(buffer: JEditBuffer): Boolean =
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    24
    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
34624
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    25
}
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    26
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    27
class IsabelleEncoding extends Encoding
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    28
{
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    29
  private val charset = Charset.forName(Isabelle_System.charset)
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    30
  private val BUFSIZE = 32768
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    31
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    32
  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    33
  {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    34
    def source(): Source =
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    35
      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
34621
6cba4b3723e4 more precise wrapping of I/O streams;
wenzelm
parents: 34620
diff changeset
    36
    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    37
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    38
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    39
	override def getTextReader(in: InputStream): Reader =
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    40
    text_reader(in, charset.newDecoder())
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    41
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    42
	override def getPermissiveTextReader(in: InputStream): Reader =
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    43
	{
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    44
		val decoder = charset.newDecoder()
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    45
		decoder.onMalformedInput(CodingErrorAction.REPLACE)
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    46
		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    47
		text_reader(in, decoder)
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    48
	}
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    49
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    50
  override def getTextWriter(out: OutputStream): Writer =
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    51
  {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    52
    val buffer = new ByteArrayOutputStream(BUFSIZE) {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    53
      override def flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    54
      {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    55
        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    56
        out.write(text.getBytes(Isabelle_System.charset))
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    57
        out.flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    58
      }
34621
6cba4b3723e4 more precise wrapping of I/O streams;
wenzelm
parents: 34620
diff changeset
    59
      override def close() { out.close() }
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    60
    }
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    61
		new OutputStreamWriter(buffer, charset.newEncoder())
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    62
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    63
}