src/Pure/ML-Systems/exn.ML
author wenzelm
Thu Sep 04 16:03:47 2008 +0200 (2008-09-04)
changeset 28124 10a1f1f4c6ae
parent 23962 e0358fac0541
child 28444 283d5e41953d
permissions -rw-r--r--
moved Multithreading.task/schedule to Concurrent/schedule.ML;
     1 (*  Title:      Pure/ML-Systems/exn.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Runtime exceptions as values.
     6 *)
     7 
     8 structure Exn =
     9 struct
    10 
    11 datatype 'a result =
    12   Result of 'a |
    13   Exn of exn;
    14 
    15 fun get_result (Result x) = SOME x
    16   | get_result _ = NONE;
    17 
    18 fun get_exn (Exn exn) = SOME exn
    19   | get_exn _ = NONE;
    20 
    21 fun capture f x = Result (f x) handle e => Exn e;
    22 
    23 fun release (Result y) = y
    24   | release (Exn e) = raise e;
    25 
    26 exception EXCEPTIONS of exn list * string;
    27 
    28 end;