src/Pure/ML-Systems/exn.ML
author wenzelm
Wed Oct 01 12:00:04 2008 +0200 (2008-10-01)
changeset 28444 283d5e41953d
parent 23962 e0358fac0541
child 28459 f6a4d913cfb1
permissions -rw-r--r--
more robust treatment of Interrupt;
added release_all, release_first;
proper signature;
     1 (*  Title:      Pure/ML-Systems/exn.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Extra support for exceptions.
     6 *)
     7 
     8 signature EXN =
     9 sig
    10   datatype 'a result = Exn of exn | Result of 'a
    11   val get_result: 'a result -> 'a option
    12   val get_exn: 'a result -> exn option
    13   val capture: ('a -> 'b) -> 'a -> 'b result
    14   val release: 'a result -> 'a
    15   exception Interrupt
    16   val proper_exn: 'a result -> exn option
    17   exception EXCEPTIONS of exn list * string
    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) = raise e;
    41 
    42 
    43 (* interrupt *)
    44 
    45 exception Interrupt = Interrupt;
    46 
    47 fun proper_exn (Result _) = NONE
    48   | proper_exn (Exn Interrupt) = NONE
    49   | proper_exn (Exn exn) = SOME exn;
    50 
    51 
    52 (* release results -- collating interrupts *)
    53 
    54 exception EXCEPTIONS of exn list * string;
    55 
    56 fun release_all results =
    57   if List.all (fn Result _ => true | _ => false) results
    58   then map (fn Result x => x) results
    59   else
    60     (case List.mapPartial proper_exn results of
    61       [] => raise Interrupt
    62     | exns => raise EXCEPTIONS (exns, ""));
    63 
    64 fun release_first results = release_all results
    65   handle EXCEPTIONS (exn :: _, _) => raise exn;
    66 
    67 end;