src/Pure/ML-Systems/exn.ML
author wenzelm
Wed Oct 01 12:00:04 2008 +0200 (2008-10-01)
changeset 28444 283d5e41953d
parent 23962 e0358fac0541
child 28459 f6a4d913cfb1
permissions -rw-r--r--
more robust treatment of Interrupt;
added release_all, release_first;
proper signature;
wenzelm@23962
     1
(*  Title:      Pure/ML-Systems/exn.ML
wenzelm@23962
     2
    ID:         $Id$
wenzelm@23962
     3
    Author:     Makarius
wenzelm@23962
     4
wenzelm@28444
     5
Extra support for exceptions.
wenzelm@23962
     6
*)
wenzelm@23962
     7
wenzelm@28444
     8
signature EXN =
wenzelm@28444
     9
sig
wenzelm@28444
    10
  datatype 'a result = Exn of exn | Result of 'a
wenzelm@28444
    11
  val get_result: 'a result -> 'a option
wenzelm@28444
    12
  val get_exn: 'a result -> exn option
wenzelm@28444
    13
  val capture: ('a -> 'b) -> 'a -> 'b result
wenzelm@28444
    14
  val release: 'a result -> 'a
wenzelm@28444
    15
  exception Interrupt
wenzelm@28444
    16
  val proper_exn: 'a result -> exn option
wenzelm@28444
    17
  exception EXCEPTIONS of exn list * string
wenzelm@28444
    18
  val release_all: 'a result list -> 'a list
wenzelm@28444
    19
  val release_first: 'a result list -> 'a list
wenzelm@28444
    20
end;
wenzelm@28444
    21
wenzelm@28444
    22
structure Exn: EXN =
wenzelm@23962
    23
struct
wenzelm@23962
    24
wenzelm@28444
    25
(* runtime exceptions as values *)
wenzelm@28444
    26
wenzelm@23962
    27
datatype 'a result =
wenzelm@23962
    28
  Result of 'a |
wenzelm@23962
    29
  Exn of exn;
wenzelm@23962
    30
wenzelm@23962
    31
fun get_result (Result x) = SOME x
wenzelm@23962
    32
  | get_result _ = NONE;
wenzelm@23962
    33
wenzelm@23962
    34
fun get_exn (Exn exn) = SOME exn
wenzelm@23962
    35
  | get_exn _ = NONE;
wenzelm@23962
    36
wenzelm@23962
    37
fun capture f x = Result (f x) handle e => Exn e;
wenzelm@23962
    38
wenzelm@23962
    39
fun release (Result y) = y
wenzelm@23962
    40
  | release (Exn e) = raise e;
wenzelm@23962
    41
wenzelm@28444
    42
wenzelm@28444
    43
(* interrupt *)
wenzelm@28444
    44
wenzelm@28444
    45
exception Interrupt = Interrupt;
wenzelm@28444
    46
wenzelm@28444
    47
fun proper_exn (Result _) = NONE
wenzelm@28444
    48
  | proper_exn (Exn Interrupt) = NONE
wenzelm@28444
    49
  | proper_exn (Exn exn) = SOME exn;
wenzelm@28444
    50
wenzelm@28444
    51
wenzelm@28444
    52
(* release results -- collating interrupts *)
wenzelm@28444
    53
wenzelm@23962
    54
exception EXCEPTIONS of exn list * string;
wenzelm@23962
    55
wenzelm@28444
    56
fun release_all results =
wenzelm@28444
    57
  if List.all (fn Result _ => true | _ => false) results
wenzelm@28444
    58
  then map (fn Result x => x) results
wenzelm@28444
    59
  else
wenzelm@28444
    60
    (case List.mapPartial proper_exn results of
wenzelm@28444
    61
      [] => raise Interrupt
wenzelm@28444
    62
    | exns => raise EXCEPTIONS (exns, ""));
wenzelm@28444
    63
wenzelm@28444
    64
fun release_first results = release_all results
wenzelm@28444
    65
  handle EXCEPTIONS (exn :: _, _) => raise exn;
wenzelm@28444
    66
wenzelm@23962
    67
end;