equal
deleted
inserted
replaced
105 } |
105 } |
106 |
106 |
107 class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String) |
107 class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String) |
108 extends Function[Isabelle_Thread, Unit] |
108 extends Function[Isabelle_Thread, Unit] |
109 { |
109 { |
110 def apply(thread: Isabelle_Thread) { handle(thread) } |
110 def apply(thread: Isabelle_Thread): Unit = handle(thread) |
111 override def toString: String = name |
111 override def toString: String = name |
112 } |
112 } |
113 |
113 |
114 def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A = |
114 def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A = |
115 if (handler == null) body |
115 if (handler == null) body |
136 thread => |
136 thread => |
137 |
137 |
138 thread.setPriority(pri) |
138 thread.setPriority(pri) |
139 thread.setDaemon(daemon) |
139 thread.setDaemon(daemon) |
140 |
140 |
141 override def run { main.run() } |
141 override def run: Unit = main.run() |
142 |
142 |
143 def is_self: Boolean = Thread.currentThread == thread |
143 def is_self: Boolean = Thread.currentThread == thread |
144 |
144 |
145 |
145 |
146 /* interrupt state */ |
146 /* interrupt state */ |