5 */ |
5 */ |
6 |
6 |
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
|
10 import isabelle._ |
|
11 |
10 import org.gjt.sp.jedit.io.Encoding |
12 import org.gjt.sp.jedit.io.Encoding |
11 import org.gjt.sp.jedit.buffer.JEditBuffer |
13 import org.gjt.sp.jedit.buffer.JEditBuffer |
12 |
14 |
13 import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction} |
15 import java.nio.charset.{Charset, CodingErrorAction} |
14 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, |
16 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, |
15 CharArrayReader, ByteArrayOutputStream} |
17 CharArrayReader, ByteArrayOutputStream} |
16 |
18 |
17 import scala.io.{Source, BufferedSource} |
19 import scala.io.{Codec, Source, BufferedSource} |
18 |
20 |
19 |
21 |
20 object Isabelle_Encoding |
22 object Isabelle_Encoding |
21 { |
23 { |
22 val NAME = "UTF-8-Isabelle" |
24 val NAME = "UTF-8-Isabelle" |
26 } |
28 } |
27 |
29 |
28 class Isabelle_Encoding extends Encoding |
30 class Isabelle_Encoding extends Encoding |
29 { |
31 { |
30 private val charset = Charset.forName(Standard_System.charset) |
32 private val charset = Charset.forName(Standard_System.charset) |
31 private val BUFSIZE = 32768 |
33 val BUFSIZE = 32768 |
32 |
34 |
33 private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader = |
35 private def text_reader(in: InputStream, codec: Codec): Reader = |
34 { |
36 { |
35 def source(): Source = |
37 val source = new BufferedSource(in)(codec) |
36 BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() }) |
|
37 new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) |
38 new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) |
38 } |
39 } |
39 |
40 |
40 override def getTextReader(in: InputStream): Reader = |
41 override def getTextReader(in: InputStream): Reader = |
41 text_reader(in, charset.newDecoder()) |
42 text_reader(in, Standard_System.codec()) |
42 |
43 |
43 override def getPermissiveTextReader(in: InputStream): Reader = |
44 override def getPermissiveTextReader(in: InputStream): Reader = |
44 { |
45 { |
45 val decoder = charset.newDecoder() |
46 val codec = Standard_System.codec() |
46 decoder.onMalformedInput(CodingErrorAction.REPLACE) |
47 codec.onMalformedInput(CodingErrorAction.REPLACE) |
47 decoder.onUnmappableCharacter(CodingErrorAction.REPLACE) |
48 codec.onUnmappableCharacter(CodingErrorAction.REPLACE) |
48 text_reader(in, decoder) |
49 text_reader(in, codec) |
49 } |
50 } |
50 |
51 |
51 override def getTextWriter(out: OutputStream): Writer = |
52 override def getTextWriter(out: OutputStream): Writer = |
52 { |
53 { |
53 val buffer = new ByteArrayOutputStream(BUFSIZE) { |
54 val buffer = new ByteArrayOutputStream(BUFSIZE) { |