--- a/src/Tools/jEdit/src/isabelle_encoding.scala Fri Aug 18 22:55:54 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Sun Aug 20 14:03:23 2017 +0200
@@ -9,58 +9,14 @@
import isabelle._
-import org.gjt.sp.jedit.io.Encoding
import org.gjt.sp.jedit.buffer.JEditBuffer
-import java.nio.charset.{Charset, CodingErrorAction}
-import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
- CharArrayReader, ByteArrayOutputStream}
-
-import scala.io.{Codec, BufferedSource}
-
object Isabelle_Encoding
{
- val NAME = "UTF-8-Isabelle"
-
def is_active(buffer: JEditBuffer): Boolean =
- buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
+ buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
def maybe_decode(buffer: JEditBuffer, s: String): String =
if (is_active(buffer)) Symbol.decode(s) else s
}
-
-class Isabelle_Encoding extends Encoding
-{
- private val BUFSIZE = 32768
-
- private def text_reader(in: InputStream, codec: Codec): Reader =
- {
- val source = new BufferedSource(in)(codec)
- new CharArrayReader(Symbol.decode(source.mkString).toArray)
- }
-
- override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())
-
- override def getPermissiveTextReader(in: InputStream): Reader =
- {
- val codec = UTF8.codec()
- codec.onMalformedInput(CodingErrorAction.REPLACE)
- codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, codec)
- }
-
- override def getTextWriter(out: OutputStream): Writer =
- {
- val buffer = new ByteArrayOutputStream(BUFSIZE) {
- override def flush()
- {
- val text = Symbol.encode(toString(UTF8.charset_name))
- out.write(UTF8.bytes(text))
- out.flush()
- }
- override def close() { out.close() }
- }
- new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
- }
-}