1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Tue Jul 22 20:03:52 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Tue Jul 22 22:18:50 2014 +0200
     1.3 @@ -59,28 +59,29 @@
     1.4  
     1.5    /* global state -- owned by Swing thread */
     1.6  
     1.7 -  private var interpreters = Map.empty[Console, Interpreter]
     1.8 +  @volatile private var interpreters = Map.empty[Console, Interpreter]
     1.9  
    1.10 -  private var global_console: Console = null
    1.11 -  private var global_out: Output = null
    1.12 -  private var global_err: Output = null
    1.13 +  @volatile private var global_console: Console = null
    1.14 +  @volatile private var global_out: Output = null
    1.15 +  @volatile private var global_err: Output = null
    1.16  
    1.17    private val console_stream = new OutputStream
    1.18    {
    1.19 -    val buf = new StringBuffer
    1.20 +    val buf = new StringBuilder
    1.21      override def flush()
    1.22      {
    1.23 -      val s = buf.synchronized { val s = buf.toString; buf.setLength(0); s }
    1.24 +      val s = buf.synchronized { val s = buf.toString; buf.clear; s }
    1.25        val str = UTF8.decode_permissive(s)
    1.26        Swing_Thread.later {
    1.27          if (global_out == null) System.out.print(str)
    1.28          else global_out.writeAttrs(null, str)
    1.29        }
    1.30 +      Thread.sleep(10)  // FIXME adhoc delay to avoid loosing output
    1.31      }
    1.32      override def close() { flush () }
    1.33      def write(byte: Int) {
    1.34        val c = byte.toChar
    1.35 -      buf.append(c)
    1.36 +      buf.synchronized { buf.append(c) }
    1.37        if (c == '\n') flush()
    1.38      }
    1.39    }