src/Pure/library.ML
changeset 23963 c2ee97a963db
parent 23937 66e1f24d655d
child 24023 6fd65e2e0dba
     1.1 --- a/src/Pure/library.ML	Tue Jul 24 19:44:33 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 24 19:44:35 2007 +0200
     1.3 @@ -32,14 +32,6 @@
     1.4    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
     1.5    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     1.6  
     1.7 -  (*exceptions*)
     1.8 -  exception EXCEPTION of exn * string
     1.9 -  datatype 'a result = Result of 'a | Exn of exn
    1.10 -  val capture: ('a -> 'b) -> 'a -> 'b result
    1.11 -  val release: 'a result -> 'a
    1.12 -  val get_result: 'a result -> 'a option
    1.13 -  val get_exn: 'a result -> exn option
    1.14 -
    1.15    (*errors*)
    1.16    exception SYS_ERROR of string
    1.17    val sys_error: string -> 'a
    1.18 @@ -269,26 +261,6 @@
    1.19    | funpow n f x = funpow (n - 1) f (f x);
    1.20  
    1.21  
    1.22 -(* exceptions *)
    1.23 -
    1.24 -exception EXCEPTION of exn * string;
    1.25 -
    1.26 -datatype 'a result =
    1.27 -  Result of 'a |
    1.28 -  Exn of exn;
    1.29 -
    1.30 -fun capture f x = Result (f x) handle e => Exn e;
    1.31 -
    1.32 -fun release (Result y) = y
    1.33 -  | release (Exn e) = raise e;
    1.34 -
    1.35 -fun get_result (Result x) = SOME x
    1.36 -  | get_result _ = NONE;
    1.37 -
    1.38 -fun get_exn (Exn exn) = SOME exn
    1.39 -  | get_exn _ = NONE;
    1.40 -
    1.41 -
    1.42  (* errors *)
    1.43  
    1.44  exception SYS_ERROR of string;
    1.45 @@ -362,9 +334,9 @@
    1.46    let
    1.47      val orig_value = ! flag;
    1.48      val _ = flag := value;
    1.49 -    val result = capture f x;
    1.50 +    val result = Exn.capture f x;
    1.51      val _ = flag := orig_value;
    1.52 -  in release result end;
    1.53 +  in Exn.release result end;
    1.54  
    1.55  fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
    1.56