| author | wenzelm |
| Sun, 03 Dec 2017 18:53:49 +0100 | |
| changeset 67120 | 491fd7f0b5df |
| 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 |
} |