added the_list, the_default
authorhaftmann
Thu Sep 08 16:08:50 2005 +0200 (2005-09-08)
changeset 173137d97f60293ae
parent 17312 159783c74f75
child 17314 04e21a27c0ad
added the_list, the_default
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Sep 08 13:24:19 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Sep 08 16:08:50 2005 +0200
     1.3 @@ -48,6 +48,8 @@
     1.4    (*options*)
     1.5    val the: 'a option -> 'a
     1.6    val these: 'a list option -> 'a list
     1.7 +  val the_default: 'a -> 'a option -> 'a
     1.8 +  val the_list: 'a option -> 'a list
     1.9    val if_none: 'a option -> 'a -> 'a
    1.10    val is_some: 'a option -> bool
    1.11    val is_none: 'a option -> bool
    1.12 @@ -353,7 +355,11 @@
    1.13  
    1.14  val the = Option.valOf;
    1.15  fun these (SOME x) = x
    1.16 -  | these _ = []
    1.17 +  | these _ = [];
    1.18 +fun the_default x (SOME y) = y
    1.19 +  | the_default x _ = x;
    1.20 +fun the_list (SOME x) = [x]
    1.21 +  | the_list _ = []
    1.22  
    1.23  (*strict!*)
    1.24  fun if_none NONE y = y