src/Pure/General/exn.ML
changeset 44247 270366301bd7
parent 44246 380a4677c55d
child 56628 a2df9de46060
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
    18   val is_interrupt: exn -> bool
    18   val is_interrupt: exn -> bool
    19   val interrupt_exn: 'a result
    19   val interrupt_exn: 'a result
    20   val is_interrupt_exn: 'a result -> bool
    20   val is_interrupt_exn: 'a result -> bool
    21   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
    21   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
    22   exception EXCEPTIONS of exn list
    22   exception EXCEPTIONS of exn list
    23   val flatten: exn -> exn list
       
    24   val flatten_list: exn list -> exn list
       
    25   val release_all: 'a result list -> 'a list
       
    26   val release_first: 'a result list -> 'a list
       
    27 end;
    23 end;
    28 
    24 
    29 structure Exn: EXN =
    25 structure Exn: EXN =
    30 struct
    26 struct
    31 
    27 
    69 
    65 
    70 fun interruptible_capture f x =
    66 fun interruptible_capture f x =
    71   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    67   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    72 
    68 
    73 
    69 
    74 (* nested exceptions *)
    70 (* concatenated exceptions *)
    75 
    71 
    76 exception EXCEPTIONS of exn list;
    72 exception EXCEPTIONS of exn list;
    77 
       
    78 fun flatten (EXCEPTIONS exns) = flatten_list exns
       
    79   | flatten exn = if is_interrupt exn then [] else [exn]
       
    80 and flatten_list exns = List.concat (map flatten exns);
       
    81 
       
    82 fun release_all results =
       
    83   if List.all (fn Res _ => true | _ => false) results
       
    84   then map (fn Res x => x) results
       
    85   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
       
    86 
       
    87 fun release_first results = release_all results
       
    88   handle EXCEPTIONS [] => interrupt ()
       
    89     | EXCEPTIONS (exn :: _) => reraise exn;
       
    90 
    73 
    91 end;
    74 end;
    92 
    75 
    93 datatype illegal = Interrupt;
    76 datatype illegal = Interrupt;
    94 
    77