author | wenzelm |
Fri, 01 Sep 2017 15:15:29 +0200 | |
changeset 66591 | 6efa351190d0 |
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 |
} |