src/Tools/jEdit/src/isabelle_encoding.scala
changeset 66457 9098c36abd1a
parent 62527 aae9a2a855e0
child 67130 b023f64e0d16
--- 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())
-  }
-}