| author | wenzelm | 
| Wed, 30 Aug 2017 15:53:35 +0200 | |
| changeset 66555 | 39257f39c7da | 
| parent 66457 | 9098c36abd1a | 
| child 67304 | 3cf05d7cf174 | 
| permissions | -rw-r--r-- | 
| 
66457
 
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
 
wenzelm 
parents: 
62527 
diff
changeset
 | 
1  | 
/* Title: Tools/jEdit/src-base/isabelle_encoding.scala  | 
| 36760 | 2  | 
Author: Makarius  | 
3  | 
||
4  | 
Isabelle encoding -- based on UTF-8.  | 
|
5  | 
*/  | 
|
| 34619 | 6  | 
|
| 
66457
 
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
 
wenzelm 
parents: 
62527 
diff
changeset
 | 
7  | 
package isabelle.jedit_base  | 
| 34619 | 8  | 
|
| 34760 | 9  | 
|
| 36015 | 10  | 
import isabelle._  | 
11  | 
||
| 34619 | 12  | 
import org.gjt.sp.jedit.io.Encoding  | 
13  | 
||
| 36015 | 14  | 
import java.nio.charset.{Charset, CodingErrorAction}
 | 
| 34620 | 15  | 
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
 | 
16  | 
CharArrayReader, ByteArrayOutputStream}  | 
|
17  | 
||
| 48277 | 18  | 
import scala.io.{Codec, BufferedSource}
 | 
| 34619 | 19  | 
|
20  | 
||
| 34738 | 21  | 
class Isabelle_Encoding extends Encoding  | 
| 34619 | 22  | 
{
 | 
| 43516 | 23  | 
private val BUFSIZE = 32768  | 
| 34620 | 24  | 
|
| 36015 | 25  | 
private def text_reader(in: InputStream, codec: Codec): Reader =  | 
| 34620 | 26  | 
  {
 | 
| 36015 | 27  | 
val source = new BufferedSource(in)(codec)  | 
| 
43695
 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
 
wenzelm 
parents: 
43661 
diff
changeset
 | 
28  | 
new CharArrayReader(Symbol.decode(source.mkString).toArray)  | 
| 34620 | 29  | 
}  | 
| 34619 | 30  | 
|
| 50203 | 31  | 
override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())  | 
| 34619 | 32  | 
|
| 37175 | 33  | 
override def getPermissiveTextReader(in: InputStream): Reader =  | 
34  | 
  {
 | 
|
| 50203 | 35  | 
val codec = UTF8.codec()  | 
| 37175 | 36  | 
codec.onMalformedInput(CodingErrorAction.REPLACE)  | 
37  | 
codec.onUnmappableCharacter(CodingErrorAction.REPLACE)  | 
|
38  | 
text_reader(in, codec)  | 
|
39  | 
}  | 
|
| 34620 | 40  | 
|
41  | 
override def getTextWriter(out: OutputStream): Writer =  | 
|
42  | 
  {
 | 
|
43  | 
    val buffer = new ByteArrayOutputStream(BUFSIZE) {
 | 
|
44  | 
override def flush()  | 
|
45  | 
      {
 | 
|
| 50203 | 46  | 
val text = Symbol.encode(toString(UTF8.charset_name))  | 
| 62527 | 47  | 
out.write(UTF8.bytes(text))  | 
| 34620 | 48  | 
out.flush()  | 
49  | 
}  | 
|
| 34621 | 50  | 
      override def close() { out.close() }
 | 
| 34620 | 51  | 
}  | 
| 50203 | 52  | 
new OutputStreamWriter(buffer, UTF8.charset.newEncoder())  | 
| 34620 | 53  | 
}  | 
| 34619 | 54  | 
}  |