author | wenzelm |
Fri, 26 Jun 2009 20:07:34 +0200 | |
changeset 34625 | 799a40faa4f1 |
parent 34624 | 5e4f33d033ba |
permissions | -rw-r--r-- |
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 |
|
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34624
diff
changeset
|
10 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
34619 | 11 |
|
34620 | 12 |
import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction} |
13 |
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, |
|
14 |
CharArrayReader, ByteArrayOutputStream} |
|
15 |
||
16 |
import scala.io.{Source, BufferedSource} |
|
34619 | 17 |
|
18 |
||
34624 | 19 |
object IsabelleEncoding |
20 |
{ |
|
21 |
val NAME = "UTF-8-Isabelle" |
|
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34624
diff
changeset
|
22 |
|
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34624
diff
changeset
|
23 |
def is_active(buffer: JEditBuffer): Boolean = |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34624
diff
changeset
|
24 |
buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME |
34624 | 25 |
} |
26 |
||
34619 | 27 |
class IsabelleEncoding extends Encoding |
28 |
{ |
|
29 |
private val charset = Charset.forName(Isabelle_System.charset) |
|
34620 | 30 |
private val BUFSIZE = 32768 |
31 |
||
32 |
private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader = |
|
33 |
{ |
|
34 |
def source(): Source = |
|
35 |
BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() }) |
|
34621 | 36 |
new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray) |
34620 | 37 |
} |
34619 | 38 |
|
39 |
override def getTextReader(in: InputStream): Reader = |
|
34620 | 40 |
text_reader(in, charset.newDecoder()) |
34619 | 41 |
|
42 |
override def getPermissiveTextReader(in: InputStream): Reader = |
|
43 |
{ |
|
44 |
val decoder = charset.newDecoder() |
|
45 |
decoder.onMalformedInput(CodingErrorAction.REPLACE) |
|
46 |
decoder.onUnmappableCharacter(CodingErrorAction.REPLACE) |
|
34620 | 47 |
text_reader(in, decoder) |
34619 | 48 |
} |
34620 | 49 |
|
50 |
override def getTextWriter(out: OutputStream): Writer = |
|
51 |
{ |
|
52 |
val buffer = new ByteArrayOutputStream(BUFSIZE) { |
|
53 |
override def flush() |
|
54 |
{ |
|
55 |
val text = Isabelle.symbols.encode(toString(Isabelle_System.charset)) |
|
56 |
out.write(text.getBytes(Isabelle_System.charset)) |
|
57 |
out.flush() |
|
58 |
} |
|
34621 | 59 |
override def close() { out.close() } |
34620 | 60 |
} |
61 |
new OutputStreamWriter(buffer, charset.newEncoder()) |
|
62 |
} |
|
34619 | 63 |
} |