# 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()
     }
   }