author | wenzelm |
Tue, 23 Aug 2011 12:20:12 +0200 | |
changeset 44385 | e7fdb008aa7d |
parent 43695 | 5130dfe1b7be |
child 48277 | f14e564fca1a |
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 |
||
36015 | 19 |
import scala.io.{Codec, Source, 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 |
|
37175 | 40 |
override def getTextReader(in: InputStream): Reader = |
36015 | 41 |
text_reader(in, Standard_System.codec()) |
34619 | 42 |
|
37175 | 43 |
override def getPermissiveTextReader(in: InputStream): Reader = |
44 |
{ |
|
45 |
val codec = Standard_System.codec() |
|
46 |
codec.onMalformedInput(CodingErrorAction.REPLACE) |
|
47 |
codec.onUnmappableCharacter(CodingErrorAction.REPLACE) |
|
48 |
text_reader(in, codec) |
|
49 |
} |
|
34620 | 50 |
|
51 |
override def getTextWriter(out: OutputStream): Writer = |
|
52 |
{ |
|
53 |
val buffer = new ByteArrayOutputStream(BUFSIZE) { |
|
54 |
override def flush() |
|
55 |
{ |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43661
diff
changeset
|
56 |
val text = Symbol.encode(toString(Standard_System.charset_name)) |
34805 | 57 |
out.write(text.getBytes(Standard_System.charset)) |
34620 | 58 |
out.flush() |
59 |
} |
|
34621 | 60 |
override def close() { out.close() } |
34620 | 61 |
} |
43516 | 62 |
new OutputStreamWriter(buffer, Standard_System.charset.newEncoder()) |
34620 | 63 |
} |
34619 | 64 |
} |