src/Pure/General/exn.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 34136 3dcb46ae6185
child 39233 9a0c67d4517a
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
     1 (*  Title:      Pure/General/exn.ML
     2     Author:     Makarius
     3 
     4 Extra support for exceptions.
     5 *)
     6 
     7 signature EXN =
     8 sig
     9   datatype 'a result = Result of 'a | Exn of exn
    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   val interrupt: unit -> 'a
    16   val is_interrupt: exn -> bool
    17   val interrupt_exn: 'a result
    18   val is_interrupt_exn: 'a result -> bool
    19   exception EXCEPTIONS of exn list
    20   val flatten: exn -> exn list
    21   val flatten_list: exn list -> exn list
    22   val release_all: 'a result list -> 'a list
    23   val release_first: 'a result list -> 'a list
    24 end;
    25 
    26 structure Exn: EXN =
    27 struct
    28 
    29 (* runtime exceptions as values *)
    30 
    31 datatype 'a result =
    32   Result of 'a |
    33   Exn of exn;
    34 
    35 fun get_result (Result x) = SOME x
    36   | get_result _ = NONE;
    37 
    38 fun get_exn (Exn exn) = SOME exn
    39   | get_exn _ = NONE;
    40 
    41 fun capture f x = Result (f x) handle e => Exn e;
    42 
    43 fun release (Result y) = y
    44   | release (Exn e) = reraise e;
    45 
    46 
    47 (* interrupts *)
    48 
    49 exception Interrupt = Interrupt;
    50 
    51 fun interrupt () = raise Interrupt;
    52 
    53 fun is_interrupt Interrupt = true
    54   | is_interrupt _ = false;
    55 
    56 val interrupt_exn = Exn Interrupt;
    57 
    58 fun is_interrupt_exn (Exn exn) = is_interrupt exn
    59   | is_interrupt_exn _ = false;
    60 
    61 
    62 (* nested exceptions *)
    63 
    64 exception EXCEPTIONS of exn list;
    65 
    66 fun flatten (EXCEPTIONS exns) = flatten_list exns
    67   | flatten exn = if is_interrupt exn then [] else [exn]
    68 and flatten_list exns = List.concat (map flatten exns);
    69 
    70 fun release_all results =
    71   if List.all (fn Result _ => true | _ => false) results
    72   then map (fn Result x => x) results
    73   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    74 
    75 fun release_first results = release_all results
    76   handle EXCEPTIONS (exn :: _) => reraise exn;
    77 
    78 end;