src/Pure/ML-Systems/exn.ML
changeset 32100 8ac6b1102f16
parent 31427 5a07cc86675d
equal deleted inserted replaced
32099:5382c93108db 32100:8ac6b1102f16
    11   val get_exn: 'a result -> exn option
    11   val get_exn: 'a result -> exn option
    12   val capture: ('a -> 'b) -> 'a -> 'b result
    12   val capture: ('a -> 'b) -> 'a -> 'b result
    13   val release: 'a result -> 'a
    13   val release: 'a result -> 'a
    14   exception Interrupt
    14   exception Interrupt
    15   exception EXCEPTIONS of exn list
    15   exception EXCEPTIONS of exn list
       
    16   val flatten: exn -> exn list
       
    17   val flatten_list: exn list -> exn list
    16   val release_all: 'a result list -> 'a list
    18   val release_all: 'a result list -> 'a list
    17   val release_first: 'a result list -> 'a list
    19   val release_first: 'a result list -> 'a list
    18 end;
    20 end;
    19 
    21 
    20 structure Exn: EXN =
    22 structure Exn: EXN =
    41 (* interrupt and nested exceptions *)
    43 (* interrupt and nested exceptions *)
    42 
    44 
    43 exception Interrupt = Interrupt;
    45 exception Interrupt = Interrupt;
    44 exception EXCEPTIONS of exn list;
    46 exception EXCEPTIONS of exn list;
    45 
    47 
    46 fun plain_exns (Result _) = []
    48 fun flatten Interrupt = []
    47   | plain_exns (Exn Interrupt) = []
    49   | flatten (EXCEPTIONS exns) = flatten_list exns
    48   | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
    50   | flatten exn = [exn]
    49   | plain_exns (Exn exn) = [exn];
    51 and flatten_list exns = List.concat (map flatten exns);
    50 
       
    51 
    52 
    52 fun release_all results =
    53 fun release_all results =
    53   if List.all (fn Result _ => true | _ => false) results
    54   if List.all (fn Result _ => true | _ => false) results
    54   then map (fn Result x => x) results
    55   then map (fn Result x => x) results
    55   else
    56   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    56     (case List.concat (map plain_exns results) of
       
    57       [] => raise Interrupt
       
    58     | exns => raise EXCEPTIONS exns);
       
    59 
    57 
    60 fun release_first results = release_all results
    58 fun release_first results = release_all results
    61   handle EXCEPTIONS (exn :: _) => reraise exn;
    59   handle EXCEPTIONS (exn :: _) => reraise exn;
    62 
    60 
    63 end;
    61 end;