added exception EXCEPTION of exn * string;
authorwenzelm
Tue Sep 13 22:19:25 2005 +0200 (2005-09-13)
changeset 17341ca0e5105c4b1
parent 17340 11f959f0fe6c
child 17342 92504e2f6c07
added exception EXCEPTION of exn * string;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Sep 13 22:19:24 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 13 22:19:25 2005 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4    val is_some: 'a option -> bool
     1.5    val is_none: 'a option -> bool
     1.6  
     1.7 +  exception EXCEPTION of exn * string
     1.8    exception ERROR
     1.9    val try: ('a -> 'b) -> 'a -> 'b option
    1.10    val can: ('a -> 'b) -> 'a -> bool
    1.11 @@ -354,10 +355,13 @@
    1.12  exception OPTION of invalid;
    1.13  
    1.14  val the = Option.valOf;
    1.15 +
    1.16  fun these (SOME x) = x
    1.17    | these _ = [];
    1.18 +
    1.19  fun the_default x (SOME y) = y
    1.20    | the_default x _ = x;
    1.21 +
    1.22  fun the_list (SOME x) = [x]
    1.23    | the_list _ = []
    1.24  
    1.25 @@ -372,7 +376,9 @@
    1.26    | is_none NONE = true;
    1.27  
    1.28  
    1.29 -(* exception handling *)
    1.30 +(* exceptions *)
    1.31 +
    1.32 +exception EXCEPTION of exn * string;
    1.33  
    1.34  exception ERROR;
    1.35  
    1.36 @@ -1281,7 +1287,8 @@
    1.37  
    1.38  fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
    1.39  
    1.40 -val rat0 = rat_of_int 0; 
    1.41 +val rat0 = rat_of_int 0;
    1.42 +
    1.43  
    1.44  (** misc **)
    1.45