src/Pure/ML-Systems/exn.ML
author berghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939 ddea202704b4
parent 23962 e0358fac0541
child 28444 283d5e41953d
permissions -rw-r--r--
Removed Logic.auto_rename.
wenzelm@23962
     1
(*  Title:      Pure/ML-Systems/exn.ML
wenzelm@23962
     2
    ID:         $Id$
wenzelm@23962
     3
    Author:     Makarius
wenzelm@23962
     4
wenzelm@23962
     5
Runtime exceptions as values.
wenzelm@23962
     6
*)
wenzelm@23962
     7
wenzelm@23962
     8
structure Exn =
wenzelm@23962
     9
struct
wenzelm@23962
    10
wenzelm@23962
    11
datatype 'a result =
wenzelm@23962
    12
  Result of 'a |
wenzelm@23962
    13
  Exn of exn;
wenzelm@23962
    14
wenzelm@23962
    15
fun get_result (Result x) = SOME x
wenzelm@23962
    16
  | get_result _ = NONE;
wenzelm@23962
    17
wenzelm@23962
    18
fun get_exn (Exn exn) = SOME exn
wenzelm@23962
    19
  | get_exn _ = NONE;
wenzelm@23962
    20
wenzelm@23962
    21
fun capture f x = Result (f x) handle e => Exn e;
wenzelm@23962
    22
wenzelm@23962
    23
fun release (Result y) = y
wenzelm@23962
    24
  | release (Exn e) = raise e;
wenzelm@23962
    25
wenzelm@23962
    26
exception EXCEPTIONS of exn list * string;
wenzelm@23962
    27
wenzelm@23962
    28
end;