src/Pure/General/exn.ML
author wenzelm
Thu Sep 09 17:38:45 2010 +0200 (2010-09-09 ago)
changeset 39233 9a0c67d4517a
parent 39232 69c6d3e87660
child 39472 1cf49add5b40
permissions -rw-r--r--
Exn.is_interrupt: include interrupts that have passed through the IO layer;
     1 (*  Title:      Pure/General/exn.ML
     2     Author:     Makarius
     3 
     4 Extra support for exceptions.
     5 *)
     6 
     7 signature EXN =
     8 sig
     9   datatype 'a result = Result of 'a | Exn of exn
    10   val get_result: 'a result -> 'a option
    11   val get_exn: 'a result -> exn option
    12   val capture: ('a -> 'b) -> 'a -> 'b result
    13   val release: 'a result -> 'a
    14   exception Interrupt
    15   val interrupt: unit -> 'a
    16   val is_interrupt: exn -> bool
    17   val interrupt_exn: 'a result
    18   val is_interrupt_exn: 'a result -> bool
    19   exception EXCEPTIONS of exn list
    20   val flatten: exn -> exn list
    21   val flatten_list: exn list -> exn list
    22   val release_all: 'a result list -> 'a list
    23   val release_first: 'a result list -> 'a list
    24 end;
    25 
    26 structure Exn: EXN =
    27 struct
    28 
    29 (* runtime exceptions as values *)
    30 
    31 datatype 'a result =
    32   Result of 'a |
    33   Exn of exn;
    34 
    35 fun get_result (Result x) = SOME x
    36   | get_result _ = NONE;
    37 
    38 fun get_exn (Exn exn) = SOME exn
    39   | get_exn _ = NONE;
    40 
    41 fun capture f x = Result (f x) handle e => Exn e;
    42 
    43 fun release (Result y) = y
    44   | release (Exn e) = reraise e;
    45 
    46 
    47 (* interrupts *)
    48 
    49 exception Interrupt = Interrupt;
    50 
    51 fun interrupt () = raise Interrupt;
    52 
    53 fun is_interrupt Interrupt = true
    54   | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
    55   | is_interrupt _ = false;
    56 
    57 val interrupt_exn = Exn Interrupt;
    58 
    59 fun is_interrupt_exn (Exn exn) = is_interrupt exn
    60   | is_interrupt_exn _ = false;
    61 
    62 
    63 (* nested exceptions *)
    64 
    65 exception EXCEPTIONS of exn list;
    66 
    67 fun flatten (EXCEPTIONS exns) = flatten_list exns
    68   | flatten exn = if is_interrupt exn then [] else [exn]
    69 and flatten_list exns = List.concat (map flatten exns);
    70 
    71 fun release_all results =
    72   if List.all (fn Result _ => true | _ => false) results
    73   then map (fn Result x => x) results
    74   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    75 
    76 fun release_first results = release_all results
    77   handle EXCEPTIONS (exn :: _) => reraise exn;
    78 
    79 end;