equal
deleted
inserted
replaced
55 def is_active(): Boolean = active && thread.isAlive |
55 def is_active(): Boolean = active && thread.isAlive |
56 def check_thread(): Boolean = Thread.currentThread == thread |
56 def check_thread(): Boolean = Thread.currentThread == thread |
57 |
57 |
58 private def failure(exn: Throwable): Unit = |
58 private def failure(exn: Throwable): Unit = |
59 Output.error_message( |
59 Output.error_message( |
60 "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn)) |
60 "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.print(exn)) |
61 |
61 |
62 private def robust_finish(): Unit = |
62 private def robust_finish(): Unit = |
63 try { finish() } catch { case exn: Throwable => failure(exn) } |
63 try { finish() } catch { case exn: Throwable => failure(exn) } |
64 |
64 |
65 |
65 |