src/Pure/ML-Systems/exn.ML
changeset 28444 283d5e41953d
parent 23962 e0358fac0541
child 28459 f6a4d913cfb1
equal deleted inserted replaced
28443:de653f1ad78b 28444:283d5e41953d
     1 (*  Title:      Pure/ML-Systems/exn.ML
     1 (*  Title:      Pure/ML-Systems/exn.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Makarius
     3     Author:     Makarius
     4 
     4 
     5 Runtime exceptions as values.
     5 Extra support for exceptions.
     6 *)
     6 *)
     7 
     7 
     8 structure Exn =
     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 =
     9 struct
    23 struct
       
    24 
       
    25 (* runtime exceptions as values *)
    10 
    26 
    11 datatype 'a result =
    27 datatype 'a result =
    12   Result of 'a |
    28   Result of 'a |
    13   Exn of exn;
    29   Exn of exn;
    14 
    30 
    21 fun capture f x = Result (f x) handle e => Exn e;
    37 fun capture f x = Result (f x) handle e => Exn e;
    22 
    38 
    23 fun release (Result y) = y
    39 fun release (Result y) = y
    24   | release (Exn e) = raise e;
    40   | release (Exn e) = raise e;
    25 
    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 
    26 exception EXCEPTIONS of exn list * string;
    54 exception EXCEPTIONS of exn list * string;
    27 
    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 
    28 end;
    67 end;