more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
authorwenzelm
Fri, 19 May 2017 18:27:11 +0200
changeset 65877 6eb1a3f7012f
parent 65876 326c9f828c3d
child 65878 effde31b1d9f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 19 18:10:55 2017 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 19 18:27:11 2017 +0200
@@ -79,18 +79,14 @@
 
   private val console_writer = new Writer
   {
-    def flush() {}
-    def close() {}
+    def flush() { console_stream.flush() }
+    def close() { console_stream.flush() }
 
     def write(cbuf: Array[Char], off: Int, len: Int)
     {
-      if (len > 0) write(new String(cbuf.slice(off, off + len)))
-    }
-
-    override def write(str: String)
-    {
-      if (global_out == null) System.out.println(str)
-      else global_out.print(null, str)
+      if (len > 0) {
+        UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
+      }
     }
   }