src/Pure/ML-Systems/exn.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32100 8ac6b1102f16
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/ML-Systems/exn.ML
     2     Author:     Makarius
     3 
     4 Extra support for exceptions.
     5 *)
     6 
     7 signature EXN =
     8 sig
     9   datatype 'a result = Exn of exn | Result of 'a
    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   exception EXCEPTIONS of exn list
    16   val flatten: exn -> exn list
    17   val flatten_list: exn list -> exn list
    18   val release_all: 'a result list -> 'a list
    19   val release_first: 'a result list -> 'a list
    20 end;
    21 
    22 structure Exn: EXN =
    23 struct
    24 
    25 (* runtime exceptions as values *)
    26 
    27 datatype 'a result =
    28   Result of 'a |
    29   Exn of exn;
    30 
    31 fun get_result (Result x) = SOME x
    32   | get_result _ = NONE;
    33 
    34 fun get_exn (Exn exn) = SOME exn
    35   | get_exn _ = NONE;
    36 
    37 fun capture f x = Result (f x) handle e => Exn e;
    38 
    39 fun release (Result y) = y
    40   | release (Exn e) = reraise e;
    41 
    42 
    43 (* interrupt and nested exceptions *)
    44 
    45 exception Interrupt = Interrupt;
    46 exception EXCEPTIONS of exn list;
    47 
    48 fun flatten Interrupt = []
    49   | flatten (EXCEPTIONS exns) = flatten_list exns
    50   | flatten exn = [exn]
    51 and flatten_list exns = List.concat (map flatten exns);
    52 
    53 fun release_all results =
    54   if List.all (fn Result _ => true | _ => false) results
    55   then map (fn Result x => x) results
    56   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    57 
    58 fun release_first results = release_all results
    59   handle EXCEPTIONS (exn :: _) => reraise exn;
    60 
    61 end;