equal
deleted
inserted
replaced
62 val str = UTF8.decode_permissive(s) |
62 val str = UTF8.decode_permissive(s) |
63 GUI_Thread.later { |
63 GUI_Thread.later { |
64 if (global_out == null) System.out.print(str) |
64 if (global_out == null) System.out.print(str) |
65 else global_out.writeAttrs(null, str) |
65 else global_out.writeAttrs(null, str) |
66 } |
66 } |
67 Thread.sleep(10) // FIXME adhoc delay to avoid loosing output |
67 Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output |
68 } |
68 } |
69 |
69 |
70 override def close() { flush () } |
70 override def close() { flush () } |
71 |
71 |
72 def write(byte: Int) |
72 def write(byte: Int) |