# HG changeset patch # User wenzelm # Date 1406060330 -7200 # Node ID 943dbbbf7ad5b089aab5810c5a7d7bb11ce96063 # Parent 5d761f9292cf8a309e85748f881beae60b51f3cb some robustification of console output; diff -r 5d761f9292cf -r 943dbbbf7ad5 src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Tue Jul 22 20:03:52 2014 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Tue Jul 22 22:18:50 2014 +0200 @@ -59,28 +59,29 @@ /* global state -- owned by Swing thread */ - private var interpreters = Map.empty[Console, Interpreter] + @volatile private var interpreters = Map.empty[Console, Interpreter] - private var global_console: Console = null - private var global_out: Output = null - private var global_err: Output = null + @volatile private var global_console: Console = null + @volatile private var global_out: Output = null + @volatile private var global_err: Output = null private val console_stream = new OutputStream { - val buf = new StringBuffer + val buf = new StringBuilder override def flush() { - val s = buf.synchronized { val s = buf.toString; buf.setLength(0); s } + val s = buf.synchronized { val s = buf.toString; buf.clear; s } val str = UTF8.decode_permissive(s) Swing_Thread.later { if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } + Thread.sleep(10) // FIXME adhoc delay to avoid loosing output } override def close() { flush () } def write(byte: Int) { val c = byte.toChar - buf.append(c) + buf.synchronized { buf.append(c) } if (c == '\n') flush() } }