src/Pure/General/exn.ML
changeset 39232 69c6d3e87660
parent 34136 3dcb46ae6185
child 39233 9a0c67d4517a
     1.1 --- a/src/Pure/General/exn.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/General/exn.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -12,6 +12,10 @@
     1.4    val capture: ('a -> 'b) -> 'a -> 'b result
     1.5    val release: 'a result -> 'a
     1.6    exception Interrupt
     1.7 +  val interrupt: unit -> 'a
     1.8 +  val is_interrupt: exn -> bool
     1.9 +  val interrupt_exn: 'a result
    1.10 +  val is_interrupt_exn: 'a result -> bool
    1.11    exception EXCEPTIONS of exn list
    1.12    val flatten: exn -> exn list
    1.13    val flatten_list: exn list -> exn list
    1.14 @@ -40,14 +44,27 @@
    1.15    | release (Exn e) = reraise e;
    1.16  
    1.17  
    1.18 -(* interrupt and nested exceptions *)
    1.19 +(* interrupts *)
    1.20  
    1.21  exception Interrupt = Interrupt;
    1.22 +
    1.23 +fun interrupt () = raise Interrupt;
    1.24 +
    1.25 +fun is_interrupt Interrupt = true
    1.26 +  | is_interrupt _ = false;
    1.27 +
    1.28 +val interrupt_exn = Exn Interrupt;
    1.29 +
    1.30 +fun is_interrupt_exn (Exn exn) = is_interrupt exn
    1.31 +  | is_interrupt_exn _ = false;
    1.32 +
    1.33 +
    1.34 +(* nested exceptions *)
    1.35 +
    1.36  exception EXCEPTIONS of exn list;
    1.37  
    1.38 -fun flatten Interrupt = []
    1.39 -  | flatten (EXCEPTIONS exns) = flatten_list exns
    1.40 -  | flatten exn = [exn]
    1.41 +fun flatten (EXCEPTIONS exns) = flatten_list exns
    1.42 +  | flatten exn = if is_interrupt exn then [] else [exn]
    1.43  and flatten_list exns = List.concat (map flatten exns);
    1.44  
    1.45  fun release_all results =