src/Pure/library.ML
changeset 17313 7d97f60293ae
parent 17257 0ab67cb765da
child 17341 ca0e5105c4b1
equal deleted inserted replaced
17312:159783c74f75 17313:7d97f60293ae
    46   exception OPTION of invalid
    46   exception OPTION of invalid
    47 
    47 
    48   (*options*)
    48   (*options*)
    49   val the: 'a option -> 'a
    49   val the: 'a option -> 'a
    50   val these: 'a list option -> 'a list
    50   val these: 'a list option -> 'a list
       
    51   val the_default: 'a -> 'a option -> 'a
       
    52   val the_list: 'a option -> 'a list
    51   val if_none: 'a option -> 'a -> 'a
    53   val if_none: 'a option -> 'a -> 'a
    52   val is_some: 'a option -> bool
    54   val is_some: 'a option -> bool
    53   val is_none: 'a option -> bool
    55   val is_none: 'a option -> bool
    54 
    56 
    55   exception ERROR
    57   exception ERROR
   351 datatype invalid = None of invalid;
   353 datatype invalid = None of invalid;
   352 exception OPTION of invalid;
   354 exception OPTION of invalid;
   353 
   355 
   354 val the = Option.valOf;
   356 val the = Option.valOf;
   355 fun these (SOME x) = x
   357 fun these (SOME x) = x
   356   | these _ = []
   358   | these _ = [];
       
   359 fun the_default x (SOME y) = y
       
   360   | the_default x _ = x;
       
   361 fun the_list (SOME x) = [x]
       
   362   | the_list _ = []
   357 
   363 
   358 (*strict!*)
   364 (*strict!*)
   359 fun if_none NONE y = y
   365 fun if_none NONE y = y
   360   | if_none (SOME x) _ = x;
   366   | if_none (SOME x) _ = x;
   361 
   367