# HG changeset patch
# User berghofe
# Date 1085168785 -7200
# Node ID 546365fe8349711812d96bf7719c43d3540d94fe
# Parent  1e83aa391ade47e30947a65fdc1d15709ec17fd4
- exported result datatype
- added functions get_result and get_exn

diff -r 1e83aa391ade -r 546365fe8349 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri May 21 21:42:05 2004 +0200
+++ b/src/Pure/library.ML	Fri May 21 21:46:25 2004 +0200
@@ -271,6 +271,9 @@
   datatype 'a error = Error of string | OK of 'a
   val get_error: 'a error -> string option
   val get_ok: 'a error -> 'a option
+  datatype 'a result = Result of 'a | Exn of exn
+  val get_result: 'a result -> 'a option
+  val get_exn: 'a result -> exn option
   val handle_error: ('a -> 'b) -> 'a -> 'b error
   exception ERROR_MESSAGE of string
   val transform_error: ('a -> 'b) -> 'a -> 'b
@@ -1238,6 +1241,12 @@
   Result of 'a |
   Exn of exn;
 
+fun get_result (Result x) = Some x
+  | get_result _ = None;
+
+fun get_exn (Exn exn) = Some exn
+  | get_exn _ = None;
+
 fun handle_error f x =
   let
     val buffer = ref ([]: string list);