equal
deleted
inserted
replaced
76 isabelle.setup.Exn.is_interrupt(exn) |
76 isabelle.setup.Exn.is_interrupt(exn) |
77 |
77 |
78 def failure_rc(exn: Throwable): Int = |
78 def failure_rc(exn: Throwable): Int = |
79 isabelle.setup.Exn.failure_rc(exn) |
79 isabelle.setup.Exn.failure_rc(exn) |
80 |
80 |
|
81 def is_interrupt_exn[A](result: Result[A]): Boolean = |
|
82 result match { |
|
83 case Exn(exn) if is_interrupt(exn) => true |
|
84 case _ => false |
|
85 } |
|
86 |
81 def interruptible_capture[A](e: => A): Result[A] = |
87 def interruptible_capture[A](e: => A): Result[A] = |
82 try { Res(e) } |
88 try { Res(e) } |
83 catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } |
89 catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } |
84 |
90 |
85 object Interrupt { |
91 object Interrupt { |