# HG changeset patch
# User wenzelm
# Date 1246033360 -7200
# Node ID 6cba4b3723e41c6691efeac6163aa970a85bbd82
# Parent  5328c64f986637ad1410c823a6bc5c028dcd765e
more precise wrapping of I/O streams;

diff -r 5328c64f9866 -r 6cba4b3723e4 src/Tools/jEdit/src/jedit/IsabelleEncoding.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleEncoding.scala	Thu Jun 25 23:54:25 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleEncoding.scala	Fri Jun 26 18:22:40 2009 +0200
@@ -24,9 +24,7 @@
   {
     def source(): Source =
       BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
-    val text = Source.fromInputStream(in, Isabelle_System.charset).mkString
-    val buffer = Isabelle.symbols.decode(text).toArray
-		new CharArrayReader(buffer)
+    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
   }
 
 	override def getTextReader(in: InputStream): Reader =
@@ -49,6 +47,7 @@
         out.write(text.getBytes(Isabelle_System.charset))
         out.flush()
       }
+      override def close() { out.close() }
     }
 		new OutputStreamWriter(buffer, charset.newEncoder())
   }