# HG changeset patch
# User wenzelm
# Date 1399056061 -7200
# Node ID d0a57abc71f8d6f4c7234f99fc6f5e716eab3dc7
# Parent  93f05fa757dd6d880b547de7603bea6a4d138c7f
clarified synchronization and exception handling;

diff -r 93f05fa757dd -r d0a57abc71f8 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:07:55 2014 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:41:01 2014 +0200
@@ -67,16 +67,20 @@
 
   private val console_stream = new OutputStream
   {
-    val buf = new StringBuilder
+    val buf = new StringBuffer
     override def flush()
     {
-      val str = UTF8.decode_permissive(buf.toString)
-      buf.clear
+      val s = buf.synchronized { val s = buf.toString; buf.setLength(0); s }
+      val str = UTF8.decode_permissive(s)
       if (global_out == null) System.out.print(str)
       else Swing_Thread.now { global_out.writeAttrs(null, str) }
     }
     override def close() { flush () }
-    def write(byte: Int) { buf.append(byte.toChar) }
+    def write(byte: Int) {
+      val c = byte.toChar
+      buf.append(c)
+      if (c == '\n') flush()
+    }
   }
 
   private val console_writer = new Writer
@@ -101,16 +105,17 @@
     global_console = console
     global_out = out
     global_err = if (err == null) out else err
-    val res = Exn.capture {
+    try {
       scala.Console.withErr(console_stream) {
         scala.Console.withOut(console_stream) { e }
       }
     }
-    console_stream.flush
-    global_console = null
-    global_out = null
-    global_err = null
-    Exn.release(res)
+    finally {
+      console_stream.flush
+      global_console = null
+      global_out = null
+      global_err = null
+    }
   }
 
   private def report_error(str: String)