author | blanchet |
Thu, 20 Nov 2014 17:29:18 +0100 | |
changeset 59018 | ec8ea2465d2a |
parent 50203 | 00d8ad713e32 |
child 62104 | fb73c0d7bb37 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
37175
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/isabelle_encoding.scala |
36760 | 2 |
Author: Makarius |
3 |
||
4 |
Isabelle encoding -- based on UTF-8. |
|
5 |
*/ |
|
34619 | 6 |
|
7 |
package isabelle.jedit |
|
8 |
||
34760 | 9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
34619 | 12 |
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
|
13 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
34619 | 14 |
|
36015 | 15 |
import java.nio.charset.{Charset, CodingErrorAction} |
34620 | 16 |
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, |
17 |
CharArrayReader, ByteArrayOutputStream} |
|
18 |
||
48277 | 19 |
import scala.io.{Codec, BufferedSource} |
34619 | 20 |
|
21 |
||
34738 | 22 |
object Isabelle_Encoding |
34624 | 23 |
{ |
24 |
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
|
25 |
|
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34624
diff
changeset
|
26 |
def is_active(buffer: JEditBuffer): Boolean = |
34793 | 27 |
buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME |
34624 | 28 |
} |
29 |
||
34738 | 30 |
class Isabelle_Encoding extends Encoding |
34619 | 31 |
{ |
43516 | 32 |
private val BUFSIZE = 32768 |
34620 | 33 |
|
36015 | 34 |
private def text_reader(in: InputStream, codec: Codec): Reader = |
34620 | 35 |
{ |
36015 | 36 |
val source = new BufferedSource(in)(codec) |
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43661
diff
changeset
|
37 |
new CharArrayReader(Symbol.decode(source.mkString).toArray) |
34620 | 38 |
} |
34619 | 39 |
|
50203 | 40 |
override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec()) |
34619 | 41 |
|
37175 | 42 |
override def getPermissiveTextReader(in: InputStream): Reader = |
43 |
{ |
|
50203 | 44 |
val codec = UTF8.codec() |
37175 | 45 |
codec.onMalformedInput(CodingErrorAction.REPLACE) |
46 |
codec.onUnmappableCharacter(CodingErrorAction.REPLACE) |
|
47 |
text_reader(in, codec) |
|
48 |
} |
|
34620 | 49 |
|
50 |
override def getTextWriter(out: OutputStream): Writer = |
|
51 |
{ |
|
52 |
val buffer = new ByteArrayOutputStream(BUFSIZE) { |
|
53 |
override def flush() |
|
54 |
{ |
|
50203 | 55 |
val text = Symbol.encode(toString(UTF8.charset_name)) |
56 |
out.write(text.getBytes(UTF8.charset)) |
|
34620 | 57 |
out.flush() |
58 |
} |
|
34621 | 59 |
override def close() { out.close() } |
34620 | 60 |
} |
50203 | 61 |
new OutputStreamWriter(buffer, UTF8.charset.newEncoder()) |
34620 | 62 |
} |
34619 | 63 |
} |