equal
deleted
inserted
replaced
45 /* thread */ |
45 /* thread */ |
46 |
46 |
47 private var active = true |
47 private var active = true |
48 private val mailbox = Mailbox[Option[Request]] |
48 private val mailbox = Mailbox[Option[Request]] |
49 |
49 |
50 private val thread = Standard_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) } |
50 private val thread = Isabelle_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) } |
51 def is_active: Boolean = active && thread.isAlive |
51 def is_active: Boolean = active && thread.isAlive |
52 def check_thread: Boolean = Thread.currentThread == thread |
52 def check_thread: Boolean = Thread.currentThread == thread |
53 |
53 |
54 private def failure(exn: Throwable): Unit = |
54 private def failure(exn: Throwable): Unit = |
55 Output.error_message( |
55 Output.error_message( |