34619
|
1 |
/*
|
|
2 |
* Isabelle encoding -- based on utf-8
|
|
3 |
*
|
|
4 |
* @author Makarius
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
import org.gjt.sp.jedit.io.Encoding
|
|
10 |
|
34620
|
11 |
import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
|
|
12 |
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
|
|
13 |
CharArrayReader, ByteArrayOutputStream}
|
|
14 |
|
|
15 |
import scala.io.{Source, BufferedSource}
|
34619
|
16 |
|
|
17 |
|
|
18 |
class IsabelleEncoding extends Encoding
|
|
19 |
{
|
|
20 |
private val charset = Charset.forName(Isabelle_System.charset)
|
34620
|
21 |
private val BUFSIZE = 32768
|
|
22 |
|
|
23 |
private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
|
|
24 |
{
|
|
25 |
def source(): Source =
|
|
26 |
BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
|
34621
|
27 |
new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
|
34620
|
28 |
}
|
34619
|
29 |
|
|
30 |
override def getTextReader(in: InputStream): Reader =
|
34620
|
31 |
text_reader(in, charset.newDecoder())
|
34619
|
32 |
|
|
33 |
override def getPermissiveTextReader(in: InputStream): Reader =
|
|
34 |
{
|
|
35 |
val decoder = charset.newDecoder()
|
|
36 |
decoder.onMalformedInput(CodingErrorAction.REPLACE)
|
|
37 |
decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
|
34620
|
38 |
text_reader(in, decoder)
|
34619
|
39 |
}
|
34620
|
40 |
|
|
41 |
override def getTextWriter(out: OutputStream): Writer =
|
|
42 |
{
|
|
43 |
val buffer = new ByteArrayOutputStream(BUFSIZE) {
|
|
44 |
override def flush()
|
|
45 |
{
|
|
46 |
val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
|
|
47 |
out.write(text.getBytes(Isabelle_System.charset))
|
|
48 |
out.flush()
|
|
49 |
}
|
34621
|
50 |
override def close() { out.close() }
|
34620
|
51 |
}
|
|
52 |
new OutputStreamWriter(buffer, charset.newEncoder())
|
|
53 |
}
|
34619
|
54 |
}
|