equal
deleted
inserted
replaced
77 /* interrupts */ |
77 /* interrupts */ |
78 |
78 |
79 def is_interrupt(exn: Throwable): Boolean = |
79 def is_interrupt(exn: Throwable): Boolean = |
80 isabelle.setup.Exn.is_interrupt(exn) |
80 isabelle.setup.Exn.is_interrupt(exn) |
81 |
81 |
|
82 def failure_rc(exn: Throwable): Int = |
|
83 isabelle.setup.Exn.failure_rc(exn) |
|
84 |
82 def interruptible_capture[A](e: => A): Result[A] = |
85 def interruptible_capture[A](e: => A): Result[A] = |
83 try { Res(e) } |
86 try { Res(e) } |
84 catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } |
87 catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } |
85 |
88 |
86 object Interrupt |
89 object Interrupt |
96 |
99 |
97 def dispose(): Unit = Thread.interrupted() |
100 def dispose(): Unit = Thread.interrupted() |
98 def expose(): Unit = if (Thread.interrupted()) throw apply() |
101 def expose(): Unit = if (Thread.interrupted()) throw apply() |
99 def impose(): Unit = Thread.currentThread.interrupt() |
102 def impose(): Unit = Thread.currentThread.interrupt() |
100 } |
103 } |
101 |
|
102 |
|
103 /* POSIX return code */ |
|
104 |
|
105 def return_code(exn: Throwable, rc: Int): Int = |
|
106 if (is_interrupt(exn)) Process_Result.interrupt_rc else rc |
|
107 |
104 |
108 |
105 |
109 /* message */ |
106 /* message */ |
110 |
107 |
111 def user_message(exn: Throwable): Option[String] = |
108 def user_message(exn: Throwable): Option[String] = |