equal
deleted
inserted
replaced
49 exception Interrupt = Interrupt; |
49 exception Interrupt = Interrupt; |
50 |
50 |
51 fun interrupt () = raise Interrupt; |
51 fun interrupt () = raise Interrupt; |
52 |
52 |
53 fun is_interrupt Interrupt = true |
53 fun is_interrupt Interrupt = true |
|
54 | is_interrupt (IO.Io {cause = Interrupt, ...}) = true |
54 | is_interrupt _ = false; |
55 | is_interrupt _ = false; |
55 |
56 |
56 val interrupt_exn = Exn Interrupt; |
57 val interrupt_exn = Exn Interrupt; |
57 |
58 |
58 fun is_interrupt_exn (Exn exn) = is_interrupt exn |
59 fun is_interrupt_exn (Exn exn) = is_interrupt exn |