equal
deleted
inserted
replaced
32 private val BUFSIZE = 32768 |
32 private val BUFSIZE = 32768 |
33 |
33 |
34 private def text_reader(in: InputStream, codec: Codec): Reader = |
34 private def text_reader(in: InputStream, codec: Codec): Reader = |
35 { |
35 { |
36 val source = new BufferedSource(in)(codec) |
36 val source = new BufferedSource(in)(codec) |
37 new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray) |
37 new CharArrayReader(Symbol.decode(source.mkString).toArray) |
38 } |
38 } |
39 |
39 |
40 override def getTextReader(in: InputStream): Reader = |
40 override def getTextReader(in: InputStream): Reader = |
41 text_reader(in, Standard_System.codec()) |
41 text_reader(in, Standard_System.codec()) |
42 |
42 |
51 override def getTextWriter(out: OutputStream): Writer = |
51 override def getTextWriter(out: OutputStream): Writer = |
52 { |
52 { |
53 val buffer = new ByteArrayOutputStream(BUFSIZE) { |
53 val buffer = new ByteArrayOutputStream(BUFSIZE) { |
54 override def flush() |
54 override def flush() |
55 { |
55 { |
56 val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name)) |
56 val text = Symbol.encode(toString(Standard_System.charset_name)) |
57 out.write(text.getBytes(Standard_System.charset)) |
57 out.write(text.getBytes(Standard_System.charset)) |
58 out.flush() |
58 out.flush() |
59 } |
59 } |
60 override def close() { out.close() } |
60 override def close() { out.close() } |
61 } |
61 } |