1/* Title: Tools/jEdit/src-base/isabelle_encoding.scala 2 Author: Makarius 3 4Isabelle encoding -- based on UTF-8. 5*/ 6 7package isabelle.jedit_base 8 9 10import isabelle._ 11 12import org.gjt.sp.jedit.io.Encoding 13 14import java.nio.charset.{Charset, CodingErrorAction, CharacterCodingException} 15import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, 16 CharArrayReader, ByteArrayOutputStream} 17 18import scala.io.{Codec, BufferedSource} 19 20 21class Isabelle_Encoding extends Encoding 22{ 23 private val BUFSIZE = 32768 24 25 private def text_reader(in: InputStream, codec: Codec, strict: Boolean): Reader = 26 { 27 val source = (new BufferedSource(in)(codec)).mkString 28 29 if (strict && Codepoint.iterator(source).exists(Symbol.is_code)) 30 throw new CharacterCodingException() 31 32 new CharArrayReader(Symbol.decode(source).toArray) 33 } 34 35 override def getTextReader(in: InputStream): Reader = 36 text_reader(in, UTF8.codec(), true) 37 38 override def getPermissiveTextReader(in: InputStream): Reader = 39 { 40 val codec = UTF8.codec() 41 codec.onMalformedInput(CodingErrorAction.REPLACE) 42 codec.onUnmappableCharacter(CodingErrorAction.REPLACE) 43 text_reader(in, codec, false) 44 } 45 46 override def getTextWriter(out: OutputStream): Writer = 47 { 48 val buffer = new ByteArrayOutputStream(BUFSIZE) { 49 override def flush() 50 { 51 val text = Symbol.encode(toString(UTF8.charset_name)) 52 out.write(UTF8.bytes(text)) 53 out.flush() 54 } 55 override def close() { out.close() } 56 } 57 new OutputStreamWriter(buffer, UTF8.charset.newEncoder()) 58 } 59} 60