src/Tools/jEdit/jedit_main/scala_console.scala
changeset 80492 43323d886ea3
parent 75702 97e8f4c938bf
child 80507 8e4731a2a041
equal deleted inserted replaced
80491:b439582efc8a 80492:43323d886ea3
    48   private val console_stream = new OutputStream {
    48   private val console_stream = new OutputStream {
    49     val buf = new StringBuilder(100)
    49     val buf = new StringBuilder(100)
    50 
    50 
    51     override def flush(): Unit = {
    51     override def flush(): Unit = {
    52       val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
    52       val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
    53       val str = UTF8.decode_permissive(s)
    53       val str = UTF8.decode_permissive(Bytes.raw(s))
    54       GUI_Thread.later {
    54       GUI_Thread.later {
    55         if (global_out == null) java.lang.System.out.print(str)
    55         if (global_out == null) java.lang.System.out.print(str)
    56         else global_out.writeAttrs(null, str)
    56         else global_out.writeAttrs(null, str)
    57       }
    57       }
    58       Time.seconds(0.01).sleep()  // FIXME adhoc delay to avoid loosing output
    58       Time.seconds(0.01).sleep()  // FIXME adhoc delay to avoid loosing output