- exported result datatype
authorberghofe
Fri May 21 21:46:25 2004 +0200 (2004-05-21)
changeset 14797546365fe8349
parent 14796 1e83aa391ade
child 14798 702cb4859cab
- exported result datatype
- added functions get_result and get_exn
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri May 21 21:42:05 2004 +0200
     1.2 +++ b/src/Pure/library.ML	Fri May 21 21:46:25 2004 +0200
     1.3 @@ -271,6 +271,9 @@
     1.4    datatype 'a error = Error of string | OK of 'a
     1.5    val get_error: 'a error -> string option
     1.6    val get_ok: 'a error -> 'a option
     1.7 +  datatype 'a result = Result of 'a | Exn of exn
     1.8 +  val get_result: 'a result -> 'a option
     1.9 +  val get_exn: 'a result -> exn option
    1.10    val handle_error: ('a -> 'b) -> 'a -> 'b error
    1.11    exception ERROR_MESSAGE of string
    1.12    val transform_error: ('a -> 'b) -> 'a -> 'b
    1.13 @@ -1238,6 +1241,12 @@
    1.14    Result of 'a |
    1.15    Exn of exn;
    1.16  
    1.17 +fun get_result (Result x) = Some x
    1.18 +  | get_result _ = None;
    1.19 +
    1.20 +fun get_exn (Exn exn) = Some exn
    1.21 +  | get_exn _ = None;
    1.22 +
    1.23  fun handle_error f x =
    1.24    let
    1.25      val buffer = ref ([]: string list);