1 /* Title: Tools/jEdit/src/jedit/isabelle_encoding.scala |
|
2 Author: Makarius |
|
3 |
|
4 Isabelle encoding -- based on UTF-8. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import org.gjt.sp.jedit.io.Encoding |
|
13 import org.gjt.sp.jedit.buffer.JEditBuffer |
|
14 |
|
15 import java.nio.charset.{Charset, CodingErrorAction} |
|
16 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, |
|
17 CharArrayReader, ByteArrayOutputStream} |
|
18 |
|
19 import scala.io.{Codec, Source, BufferedSource} |
|
20 |
|
21 |
|
22 object Isabelle_Encoding |
|
23 { |
|
24 val NAME = "UTF-8-Isabelle" |
|
25 |
|
26 def is_active(buffer: JEditBuffer): Boolean = |
|
27 buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME |
|
28 } |
|
29 |
|
30 class Isabelle_Encoding extends Encoding |
|
31 { |
|
32 private val charset = Charset.forName(Standard_System.charset) |
|
33 val BUFSIZE = 32768 |
|
34 |
|
35 private def text_reader(in: InputStream, codec: Codec): Reader = |
|
36 { |
|
37 val source = new BufferedSource(in)(codec) |
|
38 new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) |
|
39 } |
|
40 |
|
41 override def getTextReader(in: InputStream): Reader = |
|
42 text_reader(in, Standard_System.codec()) |
|
43 |
|
44 override def getPermissiveTextReader(in: InputStream): Reader = |
|
45 { |
|
46 val codec = Standard_System.codec() |
|
47 codec.onMalformedInput(CodingErrorAction.REPLACE) |
|
48 codec.onUnmappableCharacter(CodingErrorAction.REPLACE) |
|
49 text_reader(in, codec) |
|
50 } |
|
51 |
|
52 override def getTextWriter(out: OutputStream): Writer = |
|
53 { |
|
54 val buffer = new ByteArrayOutputStream(BUFSIZE) { |
|
55 override def flush() |
|
56 { |
|
57 val text = Isabelle.system.symbols.encode(toString(Standard_System.charset)) |
|
58 out.write(text.getBytes(Standard_System.charset)) |
|
59 out.flush() |
|
60 } |
|
61 override def close() { out.close() } |
|
62 } |
|
63 new OutputStreamWriter(buffer, charset.newEncoder()) |
|
64 } |
|
65 } |
|