equal
deleted
inserted
replaced
95 def unapply(exn: Throwable): Boolean = is_interrupt(exn) |
95 def unapply(exn: Throwable): Boolean = is_interrupt(exn) |
96 |
96 |
97 def dispose(): Unit = Thread.interrupted() |
97 def dispose(): Unit = Thread.interrupted() |
98 def expose(): Unit = if (Thread.interrupted()) throw apply() |
98 def expose(): Unit = if (Thread.interrupted()) throw apply() |
99 def impose(): Unit = Thread.currentThread.interrupt() |
99 def impose(): Unit = Thread.currentThread.interrupt() |
100 |
|
101 val return_code: Int = isabelle.setup.Exn.INTERRUPT_RETURN_CODE |
|
102 } |
100 } |
103 |
101 |
104 |
102 |
105 /* POSIX return code */ |
103 /* POSIX return code */ |
106 |
104 |
107 def return_code(exn: Throwable, rc: Int): Int = |
105 def return_code(exn: Throwable, rc: Int): Int = |
108 if (is_interrupt(exn)) Interrupt.return_code else rc |
106 if (is_interrupt(exn)) Process_Result.interrupt_rc else rc |
109 |
107 |
110 |
108 |
111 /* message */ |
109 /* message */ |
112 |
110 |
113 def user_message(exn: Throwable): Option[String] = |
111 def user_message(exn: Throwable): Option[String] = |