equal
deleted
inserted
replaced
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 |