src/Pure/General/basics.ML
changeset 23358 e0b5a74d7ace
parent 23225 591af6a2f09e
child 23559 0de527730294
equal deleted inserted replaced
23357:16e0ec4bcd81 23358:e0b5a74d7ace
    92 fun perhaps f x = the_default x (f x);
    92 fun perhaps f x = the_default x (f x);
    93 
    93 
    94 
    94 
    95 (* partiality *)
    95 (* partiality *)
    96 
    96 
    97 exception Interrupt = Interrupt;   (*signals intruding execution :-[*)
       
    98 
       
    99 fun try f x = SOME (f x)
    97 fun try f x = SOME (f x)
   100   handle Interrupt => raise Interrupt | _ => NONE;
    98   handle Interrupt => raise Interrupt | _ => NONE;
   101 
    99 
   102 fun can f x = is_some (try f x);
   100 fun can f x = is_some (try f x);
   103 
   101