src/Pure/ML-Systems/exn.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29564 f8b933a62151
child 31427 5a07cc86675d
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@23962
     1
(*  Title:      Pure/ML-Systems/exn.ML
wenzelm@23962
     2
    Author:     Makarius
wenzelm@23962
     3
wenzelm@28444
     4
Extra support for exceptions.
wenzelm@23962
     5
*)
wenzelm@23962
     6
wenzelm@28444
     7
signature EXN =
wenzelm@28444
     8
sig
wenzelm@28444
     9
  datatype 'a result = Exn of exn | Result of 'a
wenzelm@28444
    10
  val get_result: 'a result -> 'a option
wenzelm@28444
    11
  val get_exn: 'a result -> exn option
wenzelm@28444
    12
  val capture: ('a -> 'b) -> 'a -> 'b result
wenzelm@28444
    13
  val release: 'a result -> 'a
wenzelm@28444
    14
  exception Interrupt
wenzelm@28459
    15
  exception EXCEPTIONS of exn list
wenzelm@28444
    16
  val release_all: 'a result list -> 'a list
wenzelm@28444
    17
  val release_first: 'a result list -> 'a list
wenzelm@28444
    18
end;
wenzelm@28444
    19
wenzelm@28444
    20
structure Exn: EXN =
wenzelm@23962
    21
struct
wenzelm@23962
    22
wenzelm@28444
    23
(* runtime exceptions as values *)
wenzelm@28444
    24
wenzelm@23962
    25
datatype 'a result =
wenzelm@23962
    26
  Result of 'a |
wenzelm@23962
    27
  Exn of exn;
wenzelm@23962
    28
wenzelm@23962
    29
fun get_result (Result x) = SOME x
wenzelm@23962
    30
  | get_result _ = NONE;
wenzelm@23962
    31
wenzelm@23962
    32
fun get_exn (Exn exn) = SOME exn
wenzelm@23962
    33
  | get_exn _ = NONE;
wenzelm@23962
    34
wenzelm@23962
    35
fun capture f x = Result (f x) handle e => Exn e;
wenzelm@23962
    36
wenzelm@23962
    37
fun release (Result y) = y
wenzelm@23962
    38
  | release (Exn e) = raise e;
wenzelm@23962
    39
wenzelm@28444
    40
wenzelm@28459
    41
(* interrupt and nested exceptions *)
wenzelm@28444
    42
wenzelm@28444
    43
exception Interrupt = Interrupt;
wenzelm@28459
    44
exception EXCEPTIONS of exn list;
wenzelm@28444
    45
wenzelm@28459
    46
fun plain_exns (Result _) = []
wenzelm@28459
    47
  | plain_exns (Exn Interrupt) = []
wenzelm@28459
    48
  | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
wenzelm@28459
    49
  | plain_exns (Exn exn) = [exn];
wenzelm@28444
    50
wenzelm@23962
    51
wenzelm@28444
    52
fun release_all results =
wenzelm@28444
    53
  if List.all (fn Result _ => true | _ => false) results
wenzelm@28444
    54
  then map (fn Result x => x) results
wenzelm@28444
    55
  else
wenzelm@28459
    56
    (case List.concat (map plain_exns results) of
wenzelm@28444
    57
      [] => raise Interrupt
wenzelm@28459
    58
    | exns => raise EXCEPTIONS exns);
wenzelm@28444
    59
wenzelm@28444
    60
fun release_first results = release_all results
wenzelm@28459
    61
  handle EXCEPTIONS (exn :: _) => raise exn;
wenzelm@28444
    62
wenzelm@23962
    63
end;